git.iko.soy/Idris-dev
on master help sign in
Disjoint constants should be fatal in unification
25de16dEdwin Brady
src/Idris/Core/Unify.hs+1
compare with master
unifiedsplit
@@ -624,6 +624,7 @@ recoverable _ t@(App _ _)
624recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y
624recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y
625recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
625recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
626recoverable (Constant _) (P (DCon _ _) y _) = False
626recoverable (Constant _) (P (DCon _ _) y _) = False
627+recoverable (Constant x) (Constant y) = x == y
627recoverable (P (DCon _ _) x _) (Constant _) = False
628recoverable (P (DCon _ _) x _) (Constant _) = False
628recoverable (Constant _) (P (TCon _ _) y _) = False
629recoverable (Constant _) (P (TCon _ _) y _) = False
629recoverable (P (TCon _ _) x _) (Constant _) = False
630recoverable (P (TCon _ _) x _) (Constant _) = False