IncompleteTerm.idr

-- boilerplate functions

natToInt : Nat -> Int
natToInt Z     = 0
natToInt (S n) = 1 + (natToInt n)

natToString : Nat -> String
natToString n = show (natToInt n)

finToString : Fin n -> String
finToString f = natToString $ cast f {to = Nat}

pshow : Vect n (Fin m) -> String
pshow Nil         = ""
pshow (f :: Nil)  = (finToString f)
pshow (f :: rest) = (finToString f) ++ "  " ++ (pshow rest)

allN : (n : Nat) -> Vect n (Fin n)
allN Z     = Nil
allN (S n) = last :: (map weaken $ allN n)


-- applying in two steps works fine:

test1 : Vect 3 (Fin 3)
test1 = allN 3

test2 : String
test2 = pshow test1

-- applying in one step yields unexpected "incomplete term" error:

test3 : String
test3 = pshow $ allN 3

{-
Type checking ./error.idr
error.idr:36:7:Incomplete term pshow (allN (fromInteger 3))
Metavariables: Main.test3
-}