on master help sign in
Improve disambiguation a bit more
8173932Edwin Brady
src/Idris/Core/Unify.hs+12
@@ -688,14 +688,26 @@ recoverable _ t@(App _ _ _)
688 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
688 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
689recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
689recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
690recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
690recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
691+recoverable (TType _) (P (DCon _ _ _) y _) = False
692+recoverable (UType _) (P (DCon _ _ _) y _) = False
691recoverable (Constant _) (P (DCon _ _ _) y _) = False
693recoverable (Constant _) (P (DCon _ _ _) y _) = False
692recoverable (Constant x) (Constant y) = x == y
694recoverable (Constant x) (Constant y) = x == y
695+recoverable (P (DCon _ _ _) x _) (TType _) = False
696+recoverable (P (DCon _ _ _) x _) (UType _) = False
693recoverable (P (DCon _ _ _) x _) (Constant _) = False
697recoverable (P (DCon _ _ _) x _) (Constant _) = False
698+recoverable (TType _) (P (TCon _ _) y _) = False
699+recoverable (UType _) (P (TCon _ _) y _) = False
694recoverable (Constant _) (P (TCon _ _) y _) = False
700recoverable (Constant _) (P (TCon _ _) y _) = False
701+recoverable (P (TCon _ _) x _) (TType _) = False
702+recoverable (P (TCon _ _) x _) (UType _) = False
695recoverable (P (TCon _ _) x _) (Constant _) = False
703recoverable (P (TCon _ _) x _) (Constant _) = False
696recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False
704recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False
697recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False
705recoverable (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
698recoverable p@(Constant _) (App _ f a) = recoverable p f
708recoverable 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
699recoverable (App _ f a) p@(Constant _) = recoverable f p
711recoverable (App _ f a) p@(Constant _) = recoverable f p
700recoverable p@(P _ n _) (App _ f a) = recoverable p f
712recoverable p@(P _ n _) (App _ f a) = recoverable p f
701recoverable (App _ f a) p@(P _ _ _) = recoverable f p
713recoverable (App _ f a) p@(P _ _ _) = recoverable f p