git.iko.soy/Idris-dev
on master help sign in
Add provenance flag to unification errors

(not yet populated with any useful data)

commit426d05275e516ba8dc5e1414ac1e37a7f39caa69 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 16 Mar 2015, 16:07 (12 years ago) parent535346d
12 files changed+89−64
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+1−1 src/Idris/Core/Elaborate.hs+3−2 src/Idris/Core/ProofState.hs+31−21 src/Idris/Core/TT.hs+9−5 src/Idris/Core/Unify.hs+29−21 src/Idris/Delaborate.hs+2−2 src/Idris/Elab/Clause.hs+3−3 src/Idris/Elab/Transform.hs+2−2 src/Idris/ElabTerm.hs+3−3 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+1−1 src/Idris/TypeSearch.hs+4−2
src/Idris/AbsSyntax.hs+1−1
@@ -268,7 +268,7 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
268268
269269 where errWhen True
270270 = throwError (At fc
271− (CantUnify False x y (Msg "") [] 0))
271+ (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
272272 errWhen False = return ()
273273
274274isTyInferred :: Name -> Idris Bool
src/Idris/Core/Elaborate.hs+3−2
@@ -727,10 +727,11 @@ no_errors tac err
727727 if (length ps' > length ps) then
728728 case reverse ps' of
729729 ((x, y, _, env, inerr, while, _) : _) ->
730− let env' = map (\(x, b) -> (x, binderTy b)) env in
730+ let (xp, yp) = getProvenance inerr
731+ env' = map (\(x, b) -> (x, binderTy b)) env in
731732 lift $ tfail $
732733 case err of
733− Nothing -> CantUnify False x y inerr env' 0
734+ Nothing -> CantUnify False (x, xp) (y, yp) inerr env' 0
734735 Just e -> e
735736 else return $! ()
736737
src/Idris/Core/ProofState.hs+31−21
@@ -6,7 +6,7 @@
66
77module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
88 Tactic(..), Goal(..), processTactic, nowElaboratingPS, doneElaboratingAppPS,
9− doneElaboratingArgPS, dropGiven, keepGiven) where
9+ doneElaboratingArgPS, dropGiven, keepGiven, getProvenance) where
1010
1111import Idris.Core.Typecheck
1212import Idris.Core.Evaluate
@@ -154,9 +154,11 @@ holeName i = sMN i "hole"
154154qshow :: Fails -> String
155155qshow fs = show (map (\ (x, y, hs, _, _, _, t) -> (t, x, y, hs)) fs)
156156
157−match_unify' :: Context -> Env -> TT Name -> TT Name ->
157+match_unify' :: Context -> Env ->
158+ (TT Name, Maybe Provenance) ->
159+ (TT Name, Maybe Provenance) ->
158160 StateT TState TC [(Name, TT Name)]
159−match_unify' ctxt env topx topy =
161+match_unify' ctxt env (topx, xfrom) (topy, yfrom) =
160162 do ps <- get
161163 let while = while_elaborating ps
162164 let dont = dontunify ps
@@ -168,7 +170,7 @@ match_unify' ctxt env topx topy =
168170 ++ "\n"
169171 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"
170172 ) $
171− case match_unify ctxt env topx topy inj (holes ps) while of
173+ case match_unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps) while of
172174 OK u -> traceWhen (unifylog ps)
173175 ("Matched " ++ show u) $
174176 do let (h, ns) = unified ps
@@ -196,14 +198,16 @@ mergeSolutions env ns = merge [] ns
196198 = do ps <- get
197199 let probs = problems ps
198200 put (ps { problems = probs ++ [(t,t',True,env,
199− CantUnify True t t' (Msg "") (errEnv env) 0,
201+ CantUnify True (t, Nothing) (t', Nothing) (Msg "") (errEnv env) 0,
200202 [], Unify)] })
201203 merge acc ns
202204 | otherwise = merge ((n, t): acc) ns
203205
204−unify' :: Context -> Env -> TT Name -> TT Name ->
206+unify' :: Context -> Env ->
207+ (TT Name, Maybe Provenance) ->
208+ (TT Name, Maybe Provenance) ->
205209 StateT TState TC [(Name, TT Name)]
206−unify' ctxt env topx topy =
210+unify' ctxt env (topx, xfrom) (topy, yfrom) =
207211 do ps <- get
208212 let while = while_elaborating ps
209213 let dont = dontunify ps
@@ -216,7 +220,7 @@ unify' ctxt env topx topy =
216220 "\nHoles: " ++ show (holes ps)
217221 ++ "\nInjective: " ++ show (injective ps)
218222 ++ "\n") $
219− lift $ unify ctxt env topx topy inj (holes ps)
223+ lift $ unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps)
220224 (map fst (notunified ps)) while
221225 let notu = filter (\ (n, t) -> case t of
222226-- P _ _ _ -> False
@@ -456,7 +460,7 @@ regret ctxt env (Bind x (Hole t) _)
456460unifyGoal :: Raw -> RunTactic
457461unifyGoal tm ctxt env h@(Bind x b sc) =
458462 do (tmv, _) <- lift $ check ctxt env tm
459− ns' <- unify' ctxt env (binderTy b) tmv
463+ ns' <- unify' ctxt env (binderTy b, Nothing) (tmv, Nothing)
460464 return h
461465
462466exact :: Raw -> RunTactic
@@ -473,7 +477,7 @@ fill guess ctxt env (Bind x (Hole ty) sc) =
473477 do (val, valty) <- lift $ check ctxt env guess
474478-- let valtyn = normalise ctxt env valty
475479-- let tyn = normalise ctxt env ty
476− ns <- unify' ctxt env valty ty
480+ ns <- unify' ctxt env (valty, Nothing) (ty, Nothing)
477481 ps <- get
478482 let (uh, uns) = unified ps
479483-- put (ps { unified = (uh, uns ++ ns) })
@@ -488,7 +492,7 @@ match_fill guess ctxt env (Bind x (Hole ty) sc) =
488492 do (val, valty) <- lift $ check ctxt env guess
489493-- let valtyn = normalise ctxt env valty
490494-- let tyn = normalise ctxt env ty
491− ns <- match_unify' ctxt env valty ty
495+ ns <- match_unify' ctxt env (valty, Nothing) (ty, Nothing)
492496 ps <- get
493497 let (uh, uns) = unified ps
494498-- put (ps { unified = (uh, uns ++ ns) })
@@ -506,7 +510,7 @@ complete_fill :: RunTactic
506510complete_fill ctxt env (Bind x (Guess ty val) sc) =
507511 do let guess = forget val
508512 (val', valty) <- lift $ check ctxt env guess
509− ns <- unify' ctxt env valty ty
513+ ns <- unify' ctxt env (valty, Nothing) (ty, Nothing)
510514 ps <- get
511515 let (uh, uns) = unified ps
512516-- put (ps { unified = (uh, uns ++ ns) })
@@ -524,7 +528,7 @@ solve ctxt env (Bind x (Guess ty val) sc)
524528 dropdots <-
525529 case lookup x (notunified ps) of
526530 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
527− do match_unify' ctxt env tm val
531+ do match_unify' ctxt env (tm, Nothing) (val, Nothing)
528532 return [x]
529533 _ -> return []
530534 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
@@ -567,7 +571,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
567571-- ns <- lift $ unify ctxt env tyv t'
568572 case t' of
569573 Bind y (Pi _ s _) t -> let t' = subst y (P Bound n s) t in
570− do ns <- unify' ctxt env s tyv
574+ do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)
571575 ps <- get
572576 let (uh, uns) = unified ps
573577-- put (ps { unified = (uh, uns ++ ns) })
@@ -593,8 +597,8 @@ intro n ctxt env _ = fail "Can't introduce here."
593597forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic
594598forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
595599 do (tyv, tyt) <- lift $ check ctxt env ty
596− unify' ctxt env tyt (TType (UVar 0))
597− unify' ctxt env t (TType (UVar 0))
600+ unify' ctxt env (tyt, Nothing) (TType (UVar 0), Nothing)
601+ unify' ctxt env (t, Nothing) (TType (UVar 0), Nothing)
598602 return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))
599603forall n impl ty ctxt env _ = fail "Can't pi bind here"
600604
@@ -822,8 +826,8 @@ updateError ns (At f e) = At f (updateError ns e)
822826updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)
823827updateError ns (ElaboratingArg f a env e)
824828 = ElaboratingArg f a env (updateError ns e)
825−updateError ns (CantUnify b l r e xs sc)
826− = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc
829+updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)
830+ = CantUnify b (updateSolvedTerm ns l, lp) (updateSolvedTerm ns r, rp) (updateError ns e) xs sc
827831updateError ns e = e
828832
829833solveInProblems x val [] = []
@@ -837,7 +841,7 @@ mergeNotunified env holes ns = mnu ns [] [] where
837841 mnu ((n, t):ns) ns_acc ps_acc
838842 | Just t' <- lookup n ns, t /= t'
839843 = mnu ns ((n,t') : ns_acc)
840− ((t,t',True, env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)
844+ ((t,t',True, env,CantUnify True (t, Nothing) (t', Nothing) (Msg "") [] 0, [],Match) : ps_acc)
841845 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc
842846
843847updateNotunified [] nu = nu
@@ -846,6 +850,10 @@ updateNotunified ns nu = up nu where
846850 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in
847851 ((n, t') : up nus)
848852
853+getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
854+getProvenance (CantUnify _ (_, lp) (_, rp) _ _ _) = (lp, rp)
855+getProvenance _ = (Nothing, Nothing)
856+
849857updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
850858 -> ([(Name, TT Name)], Fails)
851859-- updateProblems ctxt [] ps inj holes = ([], ps)
@@ -860,11 +868,12 @@ updateProblems ps updates probs = up updates probs where
860868 up ns (prob@(x, y, ready, env, err, while, um) : ps) =
861869 let (x', newx) = updateSolvedTerm' ns x
862870 (y', newy) = updateSolvedTerm' ns y
871+ (lp, rp) = getProvenance err
863872 err' = updateError ns err
864873 env' = updateEnv ns env in
865874 if newx || newy || ready ||
866875 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then
867− case unify ctxt env' x' y' inj hs usupp while of
876+ case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of
868877 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v)) $
869878 up (ns ++ v) ps
870879 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $
@@ -887,9 +896,10 @@ matchProblems all ps updates probs = up updates probs where
887896 | all || um == Match =
888897 let x' = updateSolvedTerm ns x
889898 y' = updateSolvedTerm ns y
899+ (lp, rp) = getProvenance err
890900 err' = updateError ns err
891901 env' = updateEnv ns env in
892− case match_unify ctxt env' x' y' inj hs while of
902+ case match_unify ctxt env' (x', lp) (y', rp) inj hs while of
893903 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
894904 up (ns ++ v) ps
895905 _ -> let (ns', ps') = up ns ps in
src/Idris/Core/TT.hs+9−5
@@ -53,7 +53,7 @@ data FC = FC { fc_fname :: String, -- ^ Filename
5353 fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span
5454 fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span
5555 }
56− deriving (Data, Typeable)
56+ deriving (Data, Typeable, Ord)
5757
5858-- | Ignore source location equality (so deriving classes do not compare FCs)
5959instance Eq FC where
@@ -120,12 +120,16 @@ data ErrorReportPart = TextPart String
120120-- Please remember to keep Err synchronised with
121121-- Language.Reflection.Errors.Err in the stdlib!
122122
123+type Provenance = String
124+
123125-- | Idris errors. Used as exceptions in the compiler, but reported to users
124126-- if they reach the top level.
125127data Err' t
126128 = Msg String
127129 | InternalMsg String
128− | CantUnify Bool t t (Err' t) [(Name, t)] Int
130+ | CantUnify Bool (t, Maybe Provenance) -- Expected type, provenance
131+ (t, Maybe Provenance) -- Actual type, provenance
132+ (Err' t) [(Name, t)] Int
129133 -- Int is 'score' - how much we did unify
130134 -- Bool indicates recoverability, True indicates more info may make
131135 -- unification succeed
@@ -209,7 +213,7 @@ instance Sized ErrorReportPart where
209213instance Sized Err where
210214 size (Msg msg) = length msg
211215 size (InternalMsg msg) = length msg
212− size (CantUnify _ left right err _ score) = size left + size right + size err
216+ size (CantUnify _ left right err _ score) = size (fst left) + size (fst right) + size err
213217 size (InfiniteUnify _ right _) = size right
214218 size (CantConvert left right _) = size left + size right
215219 size (UnifyScope _ _ right _) = size right
@@ -261,7 +265,7 @@ instance Show Err where
261265
262266instance Pretty Err OutputAnnotation where
263267 pretty (Msg m) = text m
264− pretty (CantUnify _ l r e _ i) =
268+ pretty (CantUnify _ (l, _) (r, _) e _ i) =
265269 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>
266270 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
267271 pretty (ProviderError msg) = text msg
@@ -781,7 +785,7 @@ instance Show UExp where
781785-- | Universe constraints
782786data UConstraint = ULT UExp UExp -- ^ Strictly less than
783787 | ULE UExp UExp -- ^ Less than or equal to
784− deriving Eq
788+ deriving (Eq, Ord)
785789
786790instance Show UConstraint where
787791 show (ULT x y) = show x ++ " < " ++ show y
src/Idris/Core/Unify.hs+29−21
@@ -51,7 +51,7 @@ data UResult a = UOK a
5151 | UFail Err
5252
5353-- | Smart constructor for unification errors that takes into account the FailContext
54−cantUnify :: [FailContext] -> Bool -> t -> t -> (Err' t) -> [(Name, t)] -> Int -> Err' t
54+cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t
5555cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i
5656cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =
5757 At fc (ElaboratingArg f x
@@ -61,13 +61,15 @@ cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =
6161-- Solve metavariables by matching terms against each other
6262-- Not really unification, of course!
6363
64−match_unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] -> [FailContext] ->
64+match_unify :: Context -> Env ->
65+ (TT Name, Maybe Provenance) ->
66+ (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->
6567 TC [(Name, TT Name)]
66−match_unify ctxt env topx topy inj holes from =
68+match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
6769 case runStateT (un [] (renameBindersTm env topx)
6870 (renameBindersTm env topy)) (UI 0 []) of
6971 OK (v, UI _ []) ->
70− do v' <- trimSolutions topx topy from env v
72+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
7173 return (map (renameBinders env) v')
7274 res ->
7375 let topxn = renameBindersTm env (normalise ctxt env topx)
@@ -75,14 +77,14 @@ match_unify ctxt env topx topy inj holes from =
7577 case runStateT (un [] topxn topyn)
7678 (UI 0 []) of
7779 OK (v, UI _ fails) ->
78− do v' <- trimSolutions topx topy from env v
80+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
7981 return (map (renameBinders env) v')
8082 Error e ->
8183 -- just normalise the term we're matching against
8284 case runStateT (un [] topxn topy)
8385 (UI 0 []) of
8486 OK (v, UI _ fails) ->
85− do v' <- trimSolutions topx topy from env v
87+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
8688 return (map (renameBinders env) v')
8789 _ -> tfail e
8890 where
@@ -143,7 +145,7 @@ match_unify ctxt env topx topy inj holes from =
143145 let r = recoverable (normalise ctxt env x)
144146 (normalise ctxt env y)
145147 let err = cantUnify from r
146− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
148+ (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
147149 if (not r) then lift $ tfail err
148150 else do put (UI s ((x, y, True, env, err, from, Match) : f))
149151 lift $ tfail err
@@ -157,8 +159,9 @@ match_unify ctxt env topx topy inj holes from =
157159 uB bnames x y = do UI s f <- get
158160 let r = recoverable (normalise ctxt env (binderTy x))
159161 (normalise ctxt env (binderTy y))
160− let err = cantUnify from r topx topy
161− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
162+ let err = cantUnify from r (topx, xfrom) (topy, yfrom)
163+ (CantUnify r (binderTy x, Nothing)
164+ (binderTy y, Nothing) (Msg "") (errEnv env) s)
162165 (errEnv env) s
163166 put (UI s ((binderTy x, binderTy y,
164167 False,
@@ -179,7 +182,8 @@ match_unify ctxt env topx topy inj holes from =
179182 let r = recoverable (normalise ctxt env x)
180183 (normalise ctxt env y)
181184 let err = cantUnify from r
182− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
185+ (topx, xfrom) (topy, yfrom)
186+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
183187 put (UI s ((x, y, True, env, err, from, Match) : f))
184188 lift $ tfail err
185189 combine bnames as [] = return as
@@ -241,7 +245,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm
241245 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)
242246 explicitHole t = t
243247
244−trimSolutions topx topy from env topns = followSols [] (dropPairs topns)
248+trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPairs topns)
245249 where dropPairs [] = []
246250 dropPairs (n@(x, P _ x' _) : ns)
247251 | x == x' = dropPairs ns
@@ -258,7 +262,7 @@ trimSolutions topx topy from env topns = followSols [] (dropPairs topns)
258262 = do vs' <- case t' of
259263 P _ tn _ ->
260264 if (n, tn) `elem` vs then -- cycle
261− tfail (cantUnify from False topx topy
265+ tfail (cantUnify from False (topx, xfrom) (topy, yfrom)
262266 (Msg "") (errEnv env) 0)
263267 else return ((n, tn) : vs)
264268 _ -> return vs
@@ -280,16 +284,18 @@ hasv (App f a) = hasv f || hasv a
280284hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
281285hasv _ = False
282286
283−unify :: Context -> Env -> TT Name -> TT Name ->
287+unify :: Context -> Env ->
288+ (TT Name, Maybe Provenance) ->
289+ (TT Name, Maybe Provenance) ->
284290 [Name] -> [Name] -> [Name] -> [FailContext] ->
285291 TC ([(Name, TT Name)], Fails)
286−unify ctxt env topx topy inj holes usersupp from =
292+unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
287293-- traceWhen (hasv topx || hasv topy)
288294-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $
289295 -- don't bother if topx and topy are different at the head
290296 case runStateT (un False [] (renameBindersTm env topx)
291297 (renameBindersTm env topy)) (UI 0 []) of
292− OK (v, UI _ []) -> do v' <- trimSolutions topx topy from env v
298+ OK (v, UI _ []) -> do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
293299 return (map (renameBinders env) v', [])
294300 res ->
295301 let topxn = renameBindersTm env (normalise ctxt env topx)
@@ -298,7 +304,7 @@ unify ctxt env topx topy inj holes usersupp from =
298304 case runStateT (un False [] topxn topyn)
299305 (UI 0 []) of
300306 OK (v, UI _ fails) ->
301− do v' <- trimSolutions topx topy from env v
307+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v
302308 return (map (renameBinders env) v', reverse fails)
303309-- Error e@(CantUnify False _ _ _ _ _) -> tfail e
304310 Error e -> tfail e
@@ -470,7 +476,7 @@ unify ctxt env topx topy inj holes usersupp from =
470476 let r = recoverable (normalise ctxt env x)
471477 (normalise ctxt env y)
472478 let err = cantUnify from r
473− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
479+ (topx, xfrom) (topy, yfrom) (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
474480 if (not r) then lift $ tfail err
475481 else do put (UI s ((x, y, True, env, err, from, Unify) : f))
476482 return [] -- lift $ tfail err
@@ -569,7 +575,8 @@ unify ctxt env topx topy inj holes usersupp from =
569575 = do UI s f <- get
570576 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
571577 let err = cantUnify from r
572− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
578+ (topx, xfrom) (topy, yfrom)
579+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
573580 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
574581 return []
575582
@@ -577,7 +584,8 @@ unify ctxt env topx topy inj holes usersupp from =
577584 unifyFail x y = do UI s f <- get
578585 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)
579586 let err = cantUnify from r
580− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s
587+ (topx, xfrom) (topy, yfrom)
588+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s
581589 put (UI s ((topx, topy, True, env, err, from, Unify) : f))
582590 lift $ tfail err
583591
@@ -599,8 +607,8 @@ unify ctxt env topx topy inj holes usersupp from =
599607 uB bnames x y = do UI s f <- get
600608 let r = recoverable (normalise ctxt env (binderTy x))
601609 (normalise ctxt env (binderTy y))
602− let err = cantUnify from r topx topy
603− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)
610+ let err = cantUnify from r (topx, xfrom) (topy, yfrom)
611+ (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)
604612 (errEnv env) s
605613 put (UI s ((binderTy x, binderTy y,
606614 False,
src/Idris/Delaborate.hs+2−2
@@ -199,7 +199,7 @@ pprintErr' i (InternalMsg s) =
199199 text "This is probably a bug, or a missing error message.",
200200 text ("Please consider reporting at " ++ bugaddr)
201201 ]
202−pprintErr' i (CantUnify _ x_in y_in e sc s) =
202+pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
203203 let (x_ns, y_ns, nms) = renameMNs x_in y_in
204204 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in
205205 text "Can't unify" <> indented (annTm x_ns
@@ -212,7 +212,7 @@ pprintErr' i (CantUnify _ x_in y_in e sc s) =
212212 Msg "" -> empty
213213 -- if the specific error is the same as the one we just printed,
214214 -- there's no need to print it
215− CantUnify _ x_in' y_in' _ _ _ | x_in == x_in' && y_in == y_in' -> empty
215+ CantUnify _ (x_in', _) (y_in',_) _ _ _ | x_in == x_in' && y_in == y_in' -> empty
216216 _ -> line <> line <> text "Specifically:" <>
217217 indented (pprintErr' i e) <>
218218 if (opt_errContext (idris_options i)) then showSc i sc else empty
src/Idris/Elab/Clause.hs+3−3
@@ -464,7 +464,7 @@ checkPossible info fc tcgen fname lhs_in
464464 Error err -> if tcgen then return (recoverable ctxt err)
465465 else return (validCase ctxt err ||
466466 recoverable ctxt err)
467− where validCase ctxt (CantUnify _ topx topy e _ _)
467+ where validCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)
468468 = let topx' = normalise ctxt [] topx
469469 topy' = normalise ctxt [] topy in
470470 not (sameFam topx' topy' || not (validCase ctxt e))
@@ -474,7 +474,7 @@ checkPossible info fc tcgen fname lhs_in
474474 validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e
475475 validCase ctxt _ = True
476476
477− recoverable ctxt (CantUnify r topx topy e _ _)
477+ recoverable ctxt (CantUnify r (topx, _) (topy, _) e _ _)
478478 = let topx' = normalise ctxt [] topx
479479 topy' = normalise ctxt [] topy in
480480 checkRec topx' topy'
@@ -704,7 +704,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
704704 OK (_, cs) -> do addConstraints fc cs
705705 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs
706706 return ()
707− Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))
707+ Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))
708708 i <- getIState
709709 checkInferred fc (delab' i crhs True True) rhs
710710 -- if the function is declared '%error_reverse', or its type,
src/Idris/Elab/Transform.hs+2−2
@@ -81,12 +81,12 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
8181 -- Types must always convert
8282 case converts ctxt [] clhs_ty crhs_ty of
8383 OK _ -> return ()
84− Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))
84+ Error e -> ierror (At fc (CantUnify False (clhs_tm, Nothing) (crhs_tm, Nothing) e [] 0))
8585 -- In safe mode, values must convert (Thinks: This is probably not
8686 -- useful as is, perhaps it should require a proof of equality instead)
8787 when safe $ case converts ctxt [] clhs_tm crhs_tm of
8888 OK _ -> return ()
89− Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))
89+ Error e -> ierror (At fc (CantUnify False (clhs_tm, Nothing) (crhs_tm, Nothing) e [] 0))
9090
9191 case unApply (depat clhs_tm) of
9292 (P _ tfname _, _) -> do addTrans tfname (clhs_tm, crhs_tm)
src/Idris/ElabTerm.hs+3−3
@@ -268,10 +268,10 @@ elab ist info emode opts fn tm
268268 pimp (sUN "a") Placeholder True,
269269 pexp ct])) True
270270
271− forceErr env (CantUnify _ t t' _ _ _)
271+ forceErr env (CantUnify _ (t,_) (t',_) _ _ _)
272272 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
273273 ht == txt "Lazy'" = True
274− forceErr env (CantUnify _ t t' _ _ _)
274+ forceErr env (CantUnify _ (t,_) (t',_) _ _ _)
275275 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
276276 ht == txt "Lazy'" = True
277277 forceErr env (InfiniteUnify _ t _)
@@ -2547,7 +2547,7 @@ reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT")
25472547reflectErr :: Err -> Raw
25482548reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
25492549reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
2550−reflectErr (CantUnify b t1 t2 e ctxt i) =
2550+reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =
25512551 raw_apply (Var $ reflErrName "CantUnify")
25522552 [ rawBool b
25532553 , reflect t1
src/Idris/Prover.hs+1−1
@@ -83,7 +83,7 @@ prove opt ctxt lit n ty
8383 "Expected type:" ++ show ty)
8484 case converts ctxt [] ty pty of
8585 OK _ -> return ()
86− Error e -> ierror (CantUnify False ty pty e [] 0)
86+ Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0)
8787 ptm' <- applyOpts ptm
8888 ei <- getErasureInfo `fmap` getIState
8989 updateContext (addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False
src/Idris/REPL.hs+1−1
@@ -969,7 +969,7 @@ process fn (DebugUnify l r)
969969 = do (ltm, _) <- elabVal recinfo ERHS l
970970 (rtm, _) <- elabVal recinfo ERHS r
971971 ctxt <- getContext
972− case unify ctxt [] ltm rtm [] [] [] [] of
972+ case unify ctxt [] (ltm, Nothing) (rtm, Nothing) [] [] [] [] of
973973 OK ans -> iputStrLn (show ans)
974974 Error e -> iputStrLn (show e)
975975
src/Idris/TypeSearch.hs+4−2
@@ -278,7 +278,7 @@ inArgTys = map . first . second
278278
279279typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]
280280typeclassUnify classInfo ctxt ty tyTry = do
281− res <- tcToMaybe $ match_unify ctxt [] ty retTy [] theHoles []
281+ res <- tcToMaybe $ match_unify ctxt [] (ty, Nothing) (retTy, Nothing) [] theHoles []
282282 guard $ null (theHoles \\ map fst res)
283283 let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs
284284 return argTys'
@@ -424,7 +424,9 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
424424 unifyQueue state [] = return state
425425 unifyQueue state ((ty1, ty2) : queue) = do
426426 --trace ("go: \n" ++ show state) True `seq` return ()
427− res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state] ty1 ty2 [] (map fst $ holes state) []
427+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state]
428+ (ty1, Nothing)
429+ (ty2, Nothing) [] (map fst $ holes state) []
428430 (state', queueAdditions) <- resolveUnis res state
429431 guard $ scoreCriterion (score state')
430432 unifyQueue state' (queue ++ queueAdditions)