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

git.iko.soy/Idris-dev

Normalise types before detecting parametric args

Otherwise we miss some, and some annoying things fail as a result (notably, trying to make aliases for type classes in functions)

commit0e7c076058b080dd28a0af454d431d2d77a00f3e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 28 Jul 2015, 10:20 (11 years ago) parent80a2cee

4 files changed+7−5

compare with master

unifiedsplit

src/Idris/Core/ProofState.hs+2−1 src/Idris/Elab/Clause.hs+2−2 src/Idris/Elab/Term.hs+1−1 src/Idris/Elab/Utils.hs+2−1

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

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

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

245245 traceWhen (unifylog ps)

246246 ("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))) $

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

249250 unified = (h, ns'),

250251 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

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

544544 [t] -> t

545545 _ -> []

546− let params = getParamsInType i [] fn_is fn_ty

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

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

548548 propagateParams i params fn_ty (addImplPat i lhs_in)

549549-- let lhs = mkLHSapp $

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

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

791791 [t] -> t

792792 _ -> []

793− let params = getParamsInType i [] fn_is fn_ty

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

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

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

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

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

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

901901 case lookup n env of

902902 Nothing -> return ()

903903 Just b ->

904− case unApply (binderTy b) of

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

905905 (P _ c _, args) ->

906906 case lookupCtxtExact c (idris_classes ist) of

907907 Nothing -> return ()

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

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

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

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

139139 = do attack; patbind n

140− case unApply t of

140+ env <- get_env

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

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

142143 [] -> return ()

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