6cc3c32 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix small elaboration bug

commit6cc3c32426ad9e04f7613d01ee00e0cf087f5819 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 31 Oct 2011, 00:02 (15 years ago) parent10b88ae

2 files changed+5−2

unifiedsplit

src/Core/CoreParser.hs+1−1

@@ -19,7 +19,7 @@ idrisDef = haskellDef {

1919 opLetter = iOpLetter,

2020 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

2121 reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",

22− "do", "dsl", "import", "return", "refl",

22+ "do", "dsl", "import", "return", -- "refl",

2323 "infix", "infixl", "infixr", "prefix",

2424 "where", "with", "forall", "syntax", "proof",

2525 "using", "params", "namespace",

src/Core/Unify.hs+4−1

@@ -13,9 +13,12 @@ import Debug.Trace

1313unify :: Context -> Env -> TT Name -> TT Name -> TC [(Name, TT Name)]

1414unify ctxt env topx topy

1515 = case un' False [] (normalise ctxt env topx) (normalise ctxt env topy) of

16− OK v -> return v

16+ OK v -> return (filter notTrivial v)

1717 Error e -> tfail $ CantUnify topx topy e

1818 where

19+ notTrivial (x, P _ x' _) = x /= x'

20+ notTrivial _ = True

21+

1922 injective (P (DCon _ _) _ _) = True

2023 injective (P (TCon _ _) _ _) = True

2124 injective (App f a) = injective f