25de16d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Disjoint constants should be fatal in unification

Fixes #1390

commit25de16dacbb9d40e77b820287fc9fa4f48b765f5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 15 Jul 2014, 17:51 (12 years ago) parentc1968ed

1 file changed+1

unifiedsplit

src/Idris/Core/Unify.hs+1

@@ -624,6 +624,7 @@ recoverable _ t@(App _ _)

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

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

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

627+recoverable (Constant x) (Constant y) = x == y

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

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

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