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

git.iko.soy/Idris-dev

on master help sign in

Pi binders can never unify with Type

4932d1cEdwin Brady11 years ago

src/Idris/Core/Unify.hs+4

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

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

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

696 | (Constant _) <- f = False

697+ | TType _ <- f = False

698+ | UType _ <- f = False

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

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

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

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

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

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

700 | (Constant _) <- f = False

702 | (Constant _) <- f = False

703+ | TType _ <- f = False

704+ | UType _ <- f = False

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

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

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

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

703recoverable x y = True

707recoverable x y = True