8c93763 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Careful when unifying explicit arguments

Need to add to the "don't unify" list before applying, not after, so that thigns which are unified by return type don't get filled in prematurely.

commit8c93763b50d66c61bf4f90b1dca971c6a9fd34a7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 17 Dec 2013, 12:27 (13 years ago) parentebb4691

3 files changed+5−5

compare with master

unifiedsplit

src/Core/Elaborate.hs+1−1 src/Idris/AbsSyntax.hs+3−3 src/Idris/CaseSplit.hs+1−1

src/Core/Elaborate.hs+1−1

@@ -422,7 +422,6 @@ apply' fillt fn imps =

422422 do args <- prepare_apply fn (map fst imps)

423423 env <- get_env

424424 g <- goal

425− fillt (raw_apply fn (map Var args))

426425 -- _Don't_ solve the arguments we're specifying by hand.

427426 -- (remove from unified list before calling end_unify)

428427 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

@@ -442,6 +441,7 @@ apply' fillt fn imps =

442441 keepGiven dont hunis hs

443442 put (ES (p { dontunify = dont, unified = (n, unify),

444443 notunified = notunify ++ notunified p }, a) s prev)

444+ fillt (raw_apply fn (map Var args))

445445 ptm <- get_term

446446 g <- goal

447447-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

src/Idris/AbsSyntax.hs+3−3

@@ -650,12 +650,12 @@ inferTy = MN 0 "__Infer"

650650inferCon = MN 0 "__infer"

651651inferDecl = PDatadecl inferTy

652652 PType

653− [("", inferCon, PPi impl (MN 0 "A") PType (

654− PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))

653+ [("", inferCon, PPi impl (MN 0 "iType") PType (

654+ PPi expl (MN 0 "ival") (PRef bi (MN 0 "iType"))

655655 (PRef bi inferTy)), bi)]

656656inferOpts = []

657657

658−infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]

658+infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "iType") Placeholder True, pexp t]

659659infP = P (TCon 6 0) inferTy (TType (UVal 0))

660660

661661getInferTerm, getInferType :: Term -> Term

src/Idris/CaseSplit.hs+1−1

@@ -221,7 +221,7 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

221221 subst (PApp fc (PRef _ t) pats)

222222 | isTConName t ctxt = Placeholder -- infer types

223223 subst (PApp fc f pats) = PApp fc f (map substArg pats)

224− subst (PEq fc l r) = PEq fc (subst l) (subst r)

224+ subst (PEq fc l r) = Placeholder -- PEq fc (subst l) (subst r)

225225 subst x = x

226226

227227 substArg arg = arg { getTm = subst (getTm arg) }