4932d1c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Pi binders can never unify with Type

Make this an unrecoverable error. This helps the coverage checker and unification

commit4932d1cf632cbb32ee7d0252d5cd180a70eae977 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 1 Sep 2015, 22:28 (11 years ago) parent47db070

1 file changed+4

unifiedsplit

src/Idris/Core/Unify.hs+4

@@ -694,10 +694,14 @@ recoverable f (Bind _ (Pi _ _ _) sc)

694694 | (P (DCon _ _ _) _ _, _) <- unApply f = False

695695 | (P (TCon _ _) _ _, _) <- unApply f = False

696696 | (Constant _) <- f = False

697+ | TType _ <- f = False

698+ | UType _ <- f = False

697699recoverable (Bind _ (Pi _ _ _) sc) f

698700 | (P (DCon _ _ _) _ _, _) <- unApply f = False

699701 | (P (TCon _ _) _ _, _) <- unApply f = False

700702 | (Constant _) <- f = False

703+ | TType _ <- f = False

704+ | UType _ <- f = False

701705recoverable (Bind _ (Lam _) sc) f = recoverable sc f

702706recoverable f (Bind _ (Lam _) sc) = recoverable f sc

703707recoverable x y = True