8173932 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Improve disambiguation a bit more

Some more unrecoverable type mismatches to rule out

commit8173932927bf4d7b2af4f4f751b820ebaa7bc1fa authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 9 Jul 2015, 12:14 (11 years ago) parent86dc822

1 file changed+12

unifiedsplit

src/Idris/Core/Unify.hs+12

@@ -688,14 +688,26 @@ recoverable _ t@(App _ _ _)

688688 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

689689recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y

690690recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

691+recoverable (TType _) (P (DCon _ _ _) y _) = False

692+recoverable (UType _) (P (DCon _ _ _) y _) = False

691693recoverable (Constant _) (P (DCon _ _ _) y _) = False

692694recoverable (Constant x) (Constant y) = x == y

695+recoverable (P (DCon _ _ _) x _) (TType _) = False

696+recoverable (P (DCon _ _ _) x _) (UType _) = False

693697recoverable (P (DCon _ _ _) x _) (Constant _) = False

698+recoverable (TType _) (P (TCon _ _) y _) = False

699+recoverable (UType _) (P (TCon _ _) y _) = False

694700recoverable (Constant _) (P (TCon _ _) y _) = False

701+recoverable (P (TCon _ _) x _) (TType _) = False

702+recoverable (P (TCon _ _) x _) (UType _) = False

695703recoverable (P (TCon _ _) x _) (Constant _) = False

696704recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False

697705recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False

706+recoverable p@(TType _) (App _ f a) = recoverable p f

707+recoverable p@(UType _) (App _ f a) = recoverable p f

698708recoverable p@(Constant _) (App _ f a) = recoverable p f

709+recoverable (App _ f a) p@(TType _) = recoverable f p

710+recoverable (App _ f a) p@(UType _) = recoverable f p

699711recoverable (App _ f a) p@(Constant _) = recoverable f p

700712recoverable p@(P _ n _) (App _ f a) = recoverable p f

701713recoverable (App _ f a) p@(P _ _ _) = recoverable f p