git.iko.soy/Idris-dev
on master help sign in
Fix small elaboration bug
6cc3c32Edwin Brady
src/Core/CoreParser.hs+1−1
compare with master
unifiedsplit
@@ -19,7 +19,7 @@ idrisDef = haskellDef {
19 opLetter = iOpLetter,
19 opLetter = iOpLetter,
20 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
20 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
21 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",
21 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",
22− "do", "dsl", "import", "return", "refl",
22+ "do", "dsl", "import", "return", -- "refl",
23 "infix", "infixl", "infixr", "prefix",
23 "infix", "infixl", "infixr", "prefix",
24 "where", "with", "forall", "syntax", "proof",
24 "where", "with", "forall", "syntax", "proof",
25 "using", "params", "namespace",
25 "using", "params", "namespace",
src/Core/Unify.hs+4−1
@@ -13,9 +13,12 @@ import Debug.Trace
13unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]
13unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]
14unify ctxt env topx topy
14unify ctxt env topx topy
15 = case un' False [] (normalise ctxt env topx) (normalise ctxt env topy) of
15 = case un' False [] (normalise ctxt env topx) (normalise ctxt env topy) of
16− OK v -> return v
16+ OK v -> return (filter notTrivial v)
17 Error e -> tfail $ CantUnify topx topy e
17 Error e -> tfail $ CantUnify topx topy e
18 where
18 where
19+ notTrivial (x, P _ x' _) = x /= x'
20+ notTrivial _ = True
21+
19 injective (P (DCon _ _) _ _) = True
22 injective (P (DCon _ _) _ _) = True
20 injective (P (TCon _ _) _ _) = True
23 injective (P (TCon _ _) _ _) = True
21 injective (App f a) = injective f
24 injective (App f a) = injective f