git.iko.soy/Idris-dev
on master help sign in
Propagate unification solutions into types on 'P'

This is the source of mysterious 'No such variable' errors. Fixes #1877

commitc66df512ade939caf30d0410fd8af35f55f97c9f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 17 Mar 2015, 15:41 (12 years ago) parentbe9ffc9
5 files changed+15−4
compare with master
unifiedsplit
libs/base/Language/Reflection/Utils.idr+1 src/Idris/Core/ProofState.hs+3−1 src/Idris/Core/ProofTerm.hs+3 src/Idris/Core/TT.hs+6−1 src/Idris/Core/Unify.hs+2−2
libs/base/Language/Reflection/Utils.idr+1
@@ -272,6 +272,7 @@ instance Show Err where
272272 show (CantResolve tm) = "CantResolve " ++ show tm
273273 show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs
274274 show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm
275+ show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm
275276 show UniverseError = "UniverseError"
276277 show ProgramLineComment = "ProgramLineComment"
277278 show (Inaccessible n) = "Inaccessible " ++ show n
src/Idris/Core/ProofState.hs+3−1
@@ -940,7 +940,9 @@ processTactic EndUnify ps
940940 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns
941941 (ns'', probs') = updateProblems ps ns' (problems ps)
942942 tm' = updateSolved ns'' (pterm ps) in
943− traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'')) $
943+ traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'') ++ "\n" ++
944+ show (pterm ps) ++ "\n" ++
945+ show tm') $
944946 return (ps { pterm = tm',
945947 unified = (h, []),
946948 problems = probs',
src/Idris/Core/ProofTerm.hs+3
@@ -172,6 +172,9 @@ updateSolvedTerm' xs x = updateSolved' xs x where
172172 else (t, False)
173173 updateSolved' xs t@(P _ n@(MN _ _) _)
174174 | Just v <- lookup n xs = (v, True)
175+ updateSolved' xs t@(P nt n ty)
176+ = let (ty', ut) = updateSolved' xs ty in
177+ if ut then (P nt n ty', True) else (t, False)
175178 updateSolved' xs t = (t, False)
176179
177180 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t
src/Idris/Core/TT.hs+6−1
@@ -155,7 +155,7 @@ data Err' t
155155 | WithFnType t
156156 | NoTypeDecl Name
157157 | NotInjective t t t
158− | CantResolve Bool -- ^ True if postponed, False if fatal
158+ | CantResolve Bool -- True if postponed, False if fatal
159159 t
160160 | CantResolveAlts [Name]
161161 | IncompleteTerm t
@@ -936,6 +936,7 @@ vinstances i t = 0
936936-- | Replace the outermost (index 0) de Bruijn variable with the given term
937937instantiate :: TT n -> TT n -> TT n
938938instantiate e = subst 0 where
939+ subst i (P nt x ty) = P nt x (subst i ty)
939940 subst i (V x) | i == x = e
940941 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
941942 subst i (App f a) = App (subst i f) (subst i a)
@@ -947,6 +948,7 @@ instantiate e = subst 0 where
947948-- that has been substituted.
948949substV :: TT n -> TT n -> TT n
949950substV x tm = dropV 0 (instantiate x tm) where
951+ subst i (P nt x ty) = P nt x (subst i ty)
950952 dropV i (V x) | x > i = V (x - 1)
951953 | otherwise = V x
952954 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)
@@ -1040,6 +1042,9 @@ subst n v tm = fst $ subst' 0 tm
10401042 -- substitution happens...)
10411043 subst' i (V x) | i == x = (v, True)
10421044 subst' i (P _ x _) | n == x = (v, True)
1045+ subst' i t@(P nt x ty)
1046+ = let (ty', ut) = subst' i ty in
1047+ if ut then (P nt x ty', True) else (t, False)
10431048 subst' i t@(Bind x b sc) | x /= n
10441049 = let (b', ub) = substB' i b
10451050 (sc', usc) = subst' (i+1) sc in
src/Idris/Core/Unify.hs+2−2
@@ -100,7 +100,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
100100 | (P (TCon _ _) _ _, _) <- unApply x,
101101 holeIn env f || f `elem` holes
102102 = let n' = uniqueName (sMN 0 "mv") (map fst env) in
103− checkCycle names (f, Bind n' (Lam t) x)
103+ checkCycle names (f, Bind n' (Lam t) x)
104104 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x
105105 | (P (TCon _ _) _ _, _) <- unApply x,
106106 holeIn env f || f `elem` holes
@@ -110,7 +110,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
110110 | (P (DCon _ _ _) _ _, _) <- unApply x,
111111 holeIn env f || f `elem` holes
112112 = let n' = uniqueName (sMN 0 "mv") (map fst env) in
113− checkCycle names (f, Bind n' (Lam t) x)
113+ checkCycle names (f, Bind n' (Lam t) x)
114114 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x
115115 | (P (DCon _ _ _) _ _, _) <- unApply x,
116116 holeIn env f || f `elem` holes