git.iko.soy/Idris-dev
on master help sign in
Clearer 'incomplete term' error

e.g. Idris> [] (input):Can't infer argument elem to Prelude.List.Nil Idris> [] ++ [] (input):Can't infer argument a to Prelude.List.++, Can't infer argument a to Prelude.List.Nil

commit00bfe56039eb6154d875008a1958bfe2dd46478b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 28 Jun 2015, 16:35 (11 years ago) parent65b5c20
5 files changed+41−10
compare with master
unifiedsplit
libs/prelude/Decidable/Equality.idr+1−1 libs/prelude/Language/Reflection.idr+4−4 libs/prelude/Prelude/List.idr+2−2 src/Idris/Delaborate.hs+32−1 test/quasiquote001/expected+2−2
libs/prelude/Decidable/Equality.idr+1−1
@@ -123,7 +123,7 @@ instance (DecEq a, DecEq b) => DecEq (a, b) where
123123-- List
124124--------------------------------------------------------------------------------
125125
126−lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> Void)
126+lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {elem = t} -> Void)
127127lemma_val_not_nil Refl impossible
128128
129129lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)
libs/prelude/Language/Reflection.idr+4−4
@@ -401,13 +401,13 @@ instance Quotable NameType Raw where
401401
402402instance Quotable a TT => Quotable (List a) TT where
403403 quotedTy = `(List ~(quotedTy {a}))
404− quote [] = `(List.Nil {a=~(quotedTy {a})})
405− quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))
404+ quote [] = `(List.Nil {elem=~(quotedTy {a})})
405+ quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))
406406
407407instance Quotable a Raw => Quotable (List a) Raw where
408408 quotedTy = `(List ~(quotedTy {a}))
409− quote [] = `(List.Nil {a=~(quotedTy {a})})
410− quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))
409+ quote [] = `(List.Nil {elem=~(quotedTy {a})})
410+ quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))
411411
412412mutual
413413 instance Quotable TTName TT where
libs/prelude/Prelude/List.idr+2−2
@@ -18,11 +18,11 @@ infix 5 \\
1818infixr 7 ::,++
1919
2020||| Linked lists
21−%elim data List a =
21+%elim data List elem =
2222 ||| The empty list
2323 Nil |
2424 ||| Cons cell
25− (::) a (List a)
25+ (::) elem (List elem)
2626
2727-- Name hints for interactive editing
2828%name List xs, ys, zs, ws
src/Idris/Delaborate.hs+32−1
@@ -350,7 +350,38 @@ pprintErr' i (WithFnType ty) =
350350 text "Can't match on a function: type is" <+> annTm ty (pprintTerm i (delabSugared i ty))
351351pprintErr' i (CantMatch t) =
352352 text "Can't match on" <+> annTm t (pprintTerm i (delabSugared i t))
353−pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delabSugared i t))
353+pprintErr' i (IncompleteTerm t)
354+ = align (cat (punctuate (comma <> space)
355+ (map pprintIncomplete (nub $ getMissing [] [] t))))
356+ where
357+ pprintIncomplete (fn, arg)
358+ = text "Can't infer argument" <+> annName arg <+> text "to" <+>
359+ annName fn
360+
361+ getMissing :: [Name] -> [Name] -> Term -> [(Name, Name)]
362+ getMissing hs env (Bind n (Hole ty) sc)
363+ = getMissing (n : hs) (n : env) sc
364+ getMissing hs env (Bind n (Guess _ _) sc)
365+ = getMissing (n : hs) (n : env) sc
366+ getMissing hs env (Bind n (Let t v) sc)
367+ = getMissing hs env t ++
368+ getMissing hs env v ++
369+ getMissing hs (n : env) sc
370+ getMissing hs env (Bind n b sc)
371+ = getMissing hs env (binderTy b) ++
372+ getMissing hs (n : env) sc
373+ getMissing hs env ap@(App _ _ _)
374+ | (P _ n _, args) <- unApply ap = getMissingArgs n args
375+ where
376+ getMissingArgs n [] = []
377+ getMissingArgs n (V i : as)
378+ | env!!i `elem` hs = (n, env!!i) : getMissingArgs n as
379+ getMissingArgs n (P _ a _ : as)
380+ | a `elem` hs = (n, a) : getMissingArgs n as
381+ getMissingArgs n (a : as) = getMissing hs env a ++ getMissingArgs n as
382+ getMissing hs env (App _ f a)
383+ = getMissing hs env f ++ getMissing hs env a
384+ getMissing hs env _ = []
354385pprintErr' i (NoEliminator s t)
355386 = text "No " <> text s <> text " for type " <+>
356387 annTm t (pprintTerm i (delabSugared i t)) <$>
test/quasiquote001/expected+2−2
@@ -1,5 +1,5 @@
1−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))))
1+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar -1)))))
22--------------
3−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "a") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))
3+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar -1))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar -1)) (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))
44--------------
55App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "B") (Pi (TType (UVar -1)) (TType (UVar -1))) (Bind (UN "a") (Pi (V 1) (TType (UVar -1))) (Bind (UN "b") (Pi (V 1) (TType (UVar -1))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))