0e7c076 · Idris-dev · git.iko.soy

src/Idris/Core/ProofState.hs+2−1

compare with master

unifiedsplit

@@ -244,7 +244,8 @@ unify' ctxt env (topx, xfrom) (topy, yfrom) =

244 let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)

245 traceWhen (unifylog ps)

246 ("Now solved: " ++ show ns' ++

247− "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $

247+ "\nNow problems: " ++ qshow (probs' ++ probs_notu) ++

248+ "\nNow injective: " ++ show (updateInj u (injective ps))) $

248 put (ps { problems = probs' ++ probs_notu,

249 put (ps { problems = probs' ++ probs_notu,

249 unified = (h, ns'),

250 unified = (h, ns'),

250 injective = updateInj u (injective ps),

251 injective = updateInj u (injective ps),

src/Idris/Elab/Clause.hs+2−2

@@ -543,7 +543,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

543 let fn_is = case lookupCtxt fname (idris_implicits i) of

544 [t] -> t

545 _ -> []

546− let params = getParamsInType i [] fn_is fn_ty

546+ let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)

547 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $

548 propagateParams i params fn_ty (addImplPat i lhs_in)

549-- let lhs = mkLHSapp $

@@ -790,7 +790,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

790 let fn_is = case lookupCtxt fname (idris_implicits i) of

791 [t] -> t

792 _ -> []

793− let params = getParamsInType i [] fn_is fn_ty

793+ let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)

794 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

795 logLvl 2 ("LHS: " ++ show lhs)

796 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

src/Idris/Elab/Term.hs+1−1

@@ -901,7 +901,7 @@ elab ist info emode opts fn tm

901 case lookup n env of

902 Nothing -> return ()

903 Just b ->

904− case unApply (binderTy b) of

904+ case unApply (normalise (tt_ctxt ist) env (binderTy b)) of

905 (P _ c _, args) ->

906 case lookupCtxtExact c (idris_classes ist) of

907 Nothing -> return ()

src/Idris/Elab/Utils.hs+2−1

@@ -137,7 +137,8 @@ decorateid decorate (PClauses f o n cs)

137pbinds :: IState -> Term -> ElabD ()

138pbinds i (Bind n (PVar t) sc)

139 = do attack; patbind n

140+ env <- get_env

140− case unApply t of

141+ case unApply (normalise (tt_ctxt i) env t) of

141 (P _ c _, args) -> case lookupCtxt c (idris_classes i) of

142 (P _ c _, args) -> case lookupCtxt c (idris_classes i) of

142 [] -> return ()

143 [] -> return ()

143 _ -> -- type class, set as injective

144 _ -> -- type class, set as injective