426d052 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add provenance flag to unification errors

426d052Edwin Brady12 years ago

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -268,7 +268,7 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

268

269 where errWhen True

270 = throwError (At fc

271− (CantUnify False x y (Msg "") [] 0))

271+ (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))

272 errWhen False = return ()

273

274isTyInferred :: Name -> Idris Bool

src/Idris/Core/Elaborate.hs+3−2

@@ -727,10 +727,11 @@ no_errors tac err

727 if (length ps' > length ps) then

728 case reverse ps' of

729 ((x, y, _, env, inerr, while, _) : _) ->

730+ let (xp, yp) = getProvenance inerr

730− let env' = map (\(x, b) -> (x, binderTy b)) env in

731+ env' = map (\(x, b) -> (x, binderTy b)) env in

731 lift $ tfail $

732 lift $ tfail $

732 case err of

733 case err of

733− Nothing -> CantUnify False x y inerr env' 0

734+ Nothing -> CantUnify False (x, xp) (y, yp) inerr env' 0

734 Just e -> e

735 Just e -> e

735 else return $! ()

736 else return $! ()

736

737

src/Idris/Core/ProofState.hs+31−21

@@ -6,7 +6,7 @@

7module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

8 Tactic(..), Goal(..), processTactic, nowElaboratingPS, doneElaboratingAppPS,

9− doneElaboratingArgPS, dropGiven, keepGiven) where

9+ doneElaboratingArgPS, dropGiven, keepGiven, getProvenance) where

11import Idris.Core.Typecheck

12import Idris.Core.Evaluate

@@ -154,9 +154,11 @@ holeName i = sMN i "hole"

154qshow :: Fails -> String

155qshow fs = show (map (\ (x, y, hs, _, _, _, t) -> (t, x, y, hs)) fs)

156

157−match_unify' :: Context -> Env -> TT Name -> TT Name ->

157+match_unify' :: Context -> Env ->

158+ (TT Name, Maybe Provenance) ->

159+ (TT Name, Maybe Provenance) ->

158 StateT TState TC [(Name, TT Name)]

160 StateT TState TC [(Name, TT Name)]

159−match_unify' ctxt env topx topy =

161+match_unify' ctxt env (topx, xfrom) (topy, yfrom) =

160 do ps <- get

162 do ps <- get

161 let while = while_elaborating ps

163 let while = while_elaborating ps

162 let dont = dontunify ps

164 let dont = dontunify ps

@@ -168,7 +170,7 @@ match_unify' ctxt env topx topy =

168 ++ "\n"

170 ++ "\n"

169 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"

171 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"

170 ) $

172 ) $

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

172 OK u -> traceWhen (unifylog ps)

174 OK u -> traceWhen (unifylog ps)

173 ("Matched " ++ show u) $

175 ("Matched " ++ show u) $

174 do let (h, ns) = unified ps

176 do let (h, ns) = unified ps

@@ -196,14 +198,16 @@ mergeSolutions env ns = merge [] ns

196 = do ps <- get

198 = do ps <- get

197 let probs = problems ps

199 let probs = problems ps

198 put (ps { problems = probs ++ [(t,t',True,env,

200 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,

200 [], Unify)] })

202 [], Unify)] })

201 merge acc ns

203 merge acc ns

202 | otherwise = merge ((n, t): acc) ns

204 | otherwise = merge ((n, t): acc) ns

203

205

204−unify' :: Context -> Env -> TT Name -> TT Name ->

206+unify' :: Context -> Env ->

207+ (TT Name, Maybe Provenance) ->

208+ (TT Name, Maybe Provenance) ->

205 StateT TState TC [(Name, TT Name)]

209 StateT TState TC [(Name, TT Name)]

206−unify' ctxt env topx topy =

210+unify' ctxt env (topx, xfrom) (topy, yfrom) =

207 do ps <- get

211 do ps <- get

208 let while = while_elaborating ps

212 let while = while_elaborating ps

209 let dont = dontunify ps

213 let dont = dontunify ps

@@ -216,7 +220,7 @@ unify' ctxt env topx topy =

216 "\nHoles: " ++ show (holes ps)

220 "\nHoles: " ++ show (holes ps)

217 ++ "\nInjective: " ++ show (injective ps)

221 ++ "\nInjective: " ++ show (injective ps)

218 ++ "\n") $

222 ++ "\n") $

219− lift $ unify ctxt env topx topy inj (holes ps)

223+ lift $ unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps)

220 (map fst (notunified ps)) while

224 (map fst (notunified ps)) while

221 let notu = filter (\ (n, t) -> case t of

225 let notu = filter (\ (n, t) -> case t of

222-- P _ _ _ -> False

226-- P _ _ _ -> False

@@ -456,7 +460,7 @@ regret ctxt env (Bind x (Hole t) _)

456unifyGoal :: Raw -> RunTactic

460unifyGoal :: Raw -> RunTactic

457unifyGoal tm ctxt env h@(Bind x b sc) =

461unifyGoal tm ctxt env h@(Bind x b sc) =

458 do (tmv, _) <- lift $ check ctxt env tm

462 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)

460 return h

464 return h

461

465

462exact :: Raw -> RunTactic

466exact :: Raw -> RunTactic

@@ -473,7 +477,7 @@ fill guess ctxt env (Bind x (Hole ty) sc) =

473 do (val, valty) <- lift $ check ctxt env guess

477 do (val, valty) <- lift $ check ctxt env guess

474-- let valtyn = normalise ctxt env valty

478-- let valtyn = normalise ctxt env valty

475-- let tyn = normalise ctxt env ty

479-- let tyn = normalise ctxt env ty

476− ns <- unify' ctxt env valty ty

480+ ns <- unify' ctxt env (valty, Nothing) (ty, Nothing)

477 ps <- get

481 ps <- get

478 let (uh, uns) = unified ps

482 let (uh, uns) = unified ps

479-- put (ps { unified = (uh, uns ++ ns) })

483-- put (ps { unified = (uh, uns ++ ns) })

@@ -488,7 +492,7 @@ match_fill guess ctxt env (Bind x (Hole ty) sc) =

488 do (val, valty) <- lift $ check ctxt env guess

492 do (val, valty) <- lift $ check ctxt env guess

489-- let valtyn = normalise ctxt env valty

493-- let valtyn = normalise ctxt env valty

490-- let tyn = normalise ctxt env ty

494-- let tyn = normalise ctxt env ty

491− ns <- match_unify' ctxt env valty ty

495+ ns <- match_unify' ctxt env (valty, Nothing) (ty, Nothing)

492 ps <- get

496 ps <- get

493 let (uh, uns) = unified ps

497 let (uh, uns) = unified ps

494-- put (ps { unified = (uh, uns ++ ns) })

498-- put (ps { unified = (uh, uns ++ ns) })

@@ -506,7 +510,7 @@ complete_fill :: RunTactic

506complete_fill ctxt env (Bind x (Guess ty val) sc) =

510complete_fill ctxt env (Bind x (Guess ty val) sc) =

507 do let guess = forget val

511 do let guess = forget val

508 (val', valty) <- lift $ check ctxt env guess

512 (val', valty) <- lift $ check ctxt env guess

509− ns <- unify' ctxt env valty ty

513+ ns <- unify' ctxt env (valty, Nothing) (ty, Nothing)

510 ps <- get

514 ps <- get

511 let (uh, uns) = unified ps

515 let (uh, uns) = unified ps

512-- put (ps { unified = (uh, uns ++ ns) })

516-- put (ps { unified = (uh, uns ++ ns) })

@@ -524,7 +528,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

524 dropdots <-

528 dropdots <-

525 case lookup x (notunified ps) of

529 case lookup x (notunified ps) of

526 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

530 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)

528 return [x]

532 return [x]

529 _ -> return []

533 _ -> return []

530 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $

534 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' =

567-- ns <- lift $ unify ctxt env tyv t'

571-- ns <- lift $ unify ctxt env tyv t'

568 case t' of

572 case t' of

569 Bind y (Pi _ s _) t -> let t' = subst y (P Bound n s) t in

573 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)

571 ps <- get

575 ps <- get

572 let (uh, uns) = unified ps

576 let (uh, uns) = unified ps

573-- put (ps { unified = (uh, uns ++ ns) })

577-- put (ps { unified = (uh, uns ++ ns) })

@@ -593,8 +597,8 @@ intro n ctxt env _ = fail "Can't introduce here."

593forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic

597forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic

594forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

598forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

595 do (tyv, tyt) <- lift $ check ctxt env ty

599 do (tyv, tyt) <- lift $ check ctxt env ty

596− unify' ctxt env tyt (TType (UVar 0))

600+ unify' ctxt env (tyt, Nothing) (TType (UVar 0), Nothing)

597− unify' ctxt env t (TType (UVar 0))

601+ unify' ctxt env (t, Nothing) (TType (UVar 0), Nothing)

598 return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

602 return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))

599forall n impl ty ctxt env _ = fail "Can't pi bind here"

603forall n impl ty ctxt env _ = fail "Can't pi bind here"

600

604

@@ -822,8 +826,8 @@ updateError ns (At f e) = At f (updateError ns e)

822updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

826updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

823updateError ns (ElaboratingArg f a env e)

827updateError ns (ElaboratingArg f a env e)

824 = ElaboratingArg f a env (updateError ns e)

828 = ElaboratingArg f a env (updateError ns e)

825−updateError ns (CantUnify b l r e xs sc)

829+updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)

826− = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc

830+ = CantUnify b (updateSolvedTerm ns l, lp) (updateSolvedTerm ns r, rp) (updateError ns e) xs sc

827updateError ns e = e

831updateError ns e = e

828

832

829solveInProblems x val [] = []

833solveInProblems x val [] = []

@@ -837,7 +841,7 @@ mergeNotunified env holes ns = mnu ns [] [] where

837 mnu ((n, t):ns) ns_acc ps_acc

841 mnu ((n, t):ns) ns_acc ps_acc

838 | Just t' <- lookup n ns, t /= t'

842 | Just t' <- lookup n ns, t /= t'

839 = mnu ns ((n,t') : ns_acc)

843 = 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)

841 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

845 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

842

846

843updateNotunified [] nu = nu

847updateNotunified [] nu = nu

@@ -846,6 +850,10 @@ updateNotunified ns nu = up nu where

846 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in

850 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in

847 ((n, t') : up nus)

851 ((n, t') : up nus)

848

852

853+getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)

854+getProvenance (CantUnify _ (_, lp) (_, rp) _ _ _) = (lp, rp)

855+getProvenance _ = (Nothing, Nothing)

856+

849updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

857updateProblems :: ProofState -> [(Name, TT Name)] -> Fails

850 -> ([(Name, TT Name)], Fails)

858 -> ([(Name, TT Name)], Fails)

851-- updateProblems ctxt [] ps inj holes = ([], ps)

859-- updateProblems ctxt [] ps inj holes = ([], ps)

@@ -860,11 +868,12 @@ updateProblems ps updates probs = up updates probs where

860 up ns (prob@(x, y, ready, env, err, while, um) : ps) =

868 up ns (prob@(x, y, ready, env, err, while, um) : ps) =

861 let (x', newx) = updateSolvedTerm' ns x

869 let (x', newx) = updateSolvedTerm' ns x

862 (y', newy) = updateSolvedTerm' ns y

870 (y', newy) = updateSolvedTerm' ns y

871+ (lp, rp) = getProvenance err

863 err' = updateError ns err

872 err' = updateError ns err

864 env' = updateEnv ns env in

873 env' = updateEnv ns env in

865 if newx || newy || ready ||

874 if newx || newy || ready ||

866 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

875 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

868 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v)) $

877 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v)) $

869 up (ns ++ v) ps

878 up (ns ++ v) ps

870 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

879 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

@@ -887,9 +896,10 @@ matchProblems all ps updates probs = up updates probs where

887 | all || um == Match =

896 | all || um == Match =

888 let x' = updateSolvedTerm ns x

897 let x' = updateSolvedTerm ns x

889 y' = updateSolvedTerm ns y

898 y' = updateSolvedTerm ns y

899+ (lp, rp) = getProvenance err

890 err' = updateError ns err

900 err' = updateError ns err

891 env' = updateEnv ns env in

901 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

893 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

903 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

894 up (ns ++ v) ps

904 up (ns ++ v) ps

895 _ -> let (ns', ps') = up ns ps in

905 _ -> 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

53 fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span

54 fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span

55 }

56− deriving (Data, Typeable)

56+ deriving (Data, Typeable, Ord)

58-- | Ignore source location equality (so deriving classes do not compare FCs)

59instance Eq FC where

@@ -120,12 +120,16 @@ data ErrorReportPart = TextPart String

120-- Please remember to keep Err synchronised with

121-- Language.Reflection.Errors.Err in the stdlib!

122

123+type Provenance = String

124+

123-- | Idris errors. Used as exceptions in the compiler, but reported to users

125-- | Idris errors. Used as exceptions in the compiler, but reported to users

124-- if they reach the top level.

126-- if they reach the top level.

125data Err' t

127data Err' t

126 = Msg String

128 = Msg String

127 | InternalMsg String

129 | InternalMsg String

130+ | CantUnify Bool (t, Maybe Provenance) -- Expected type, provenance

131+ (t, Maybe Provenance) -- Actual type, provenance

128− | CantUnify Bool t t (Err' t) [(Name, t)] Int

132+ (Err' t) [(Name, t)] Int

129 -- Int is 'score' - how much we did unify

133 -- Int is 'score' - how much we did unify

130 -- Bool indicates recoverability, True indicates more info may make

134 -- Bool indicates recoverability, True indicates more info may make

131 -- unification succeed

135 -- unification succeed

@@ -209,7 +213,7 @@ instance Sized ErrorReportPart where

209instance Sized Err where

213instance Sized Err where

210 size (Msg msg) = length msg

214 size (Msg msg) = length msg

211 size (InternalMsg msg) = length msg

215 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

213 size (InfiniteUnify _ right _) = size right

217 size (InfiniteUnify _ right _) = size right

214 size (CantConvert left right _) = size left + size right

218 size (CantConvert left right _) = size left + size right

215 size (UnifyScope _ _ right _) = size right

219 size (UnifyScope _ _ right _) = size right

@@ -261,7 +265,7 @@ instance Show Err where

261

265

262instance Pretty Err OutputAnnotation where

266instance Pretty Err OutputAnnotation where

263 pretty (Msg m) = text m

267 pretty (Msg m) = text m

264− pretty (CantUnify _ l r e _ i) =

268+ pretty (CantUnify _ (l, _) (r, _) e _ i) =

265 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

269 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

266 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

270 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

267 pretty (ProviderError msg) = text msg

271 pretty (ProviderError msg) = text msg

@@ -781,7 +785,7 @@ instance Show UExp where

781-- | Universe constraints

785-- | Universe constraints

782data UConstraint = ULT UExp UExp -- ^ Strictly less than

786data UConstraint = ULT UExp UExp -- ^ Strictly less than

783 | ULE UExp UExp -- ^ Less than or equal to

787 | ULE UExp UExp -- ^ Less than or equal to

784− deriving Eq

788+ deriving (Eq, Ord)

785

789

786instance Show UConstraint where

790instance Show UConstraint where

787 show (ULT x y) = show x ++ " < " ++ show y

791 show (ULT x y) = show x ++ " < " ++ show y

src/Idris/Core/Unify.hs+29−21

@@ -51,7 +51,7 @@ data UResult a = UOK a

51 | UFail Err

53-- | 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

55cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i

56cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =

57 At fc (ElaboratingArg f x

@@ -61,13 +61,15 @@ cantUnify (FailContext fc f x : prev) r t1 t2 e ctxt i =

61-- Solve metavariables by matching terms against each other

62-- Not really unification, of course!

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] ->

65 TC [(Name, TT Name)]

67 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 =

67 case runStateT (un [] (renameBindersTm env topx)

69 case runStateT (un [] (renameBindersTm env topx)

68 (renameBindersTm env topy)) (UI 0 []) of

70 (renameBindersTm env topy)) (UI 0 []) of

69 OK (v, UI _ []) ->

71 OK (v, UI _ []) ->

70− do v' <- trimSolutions topx topy from env v

72+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

71 return (map (renameBinders env) v')

73 return (map (renameBinders env) v')

72 res ->

74 res ->

73 let topxn = renameBindersTm env (normalise ctxt env topx)

75 let topxn = renameBindersTm env (normalise ctxt env topx)

@@ -75,14 +77,14 @@ match_unify ctxt env topx topy inj holes from =

75 case runStateT (un [] topxn topyn)

77 case runStateT (un [] topxn topyn)

76 (UI 0 []) of

78 (UI 0 []) of

77 OK (v, UI _ fails) ->

79 OK (v, UI _ fails) ->

78− do v' <- trimSolutions topx topy from env v

80+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

79 return (map (renameBinders env) v')

81 return (map (renameBinders env) v')

80 Error e ->

82 Error e ->

81 -- just normalise the term we're matching against

83 -- just normalise the term we're matching against

82 case runStateT (un [] topxn topy)

84 case runStateT (un [] topxn topy)

83 (UI 0 []) of

85 (UI 0 []) of

84 OK (v, UI _ fails) ->

86 OK (v, UI _ fails) ->

85− do v' <- trimSolutions topx topy from env v

87+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

86 return (map (renameBinders env) v')

88 return (map (renameBinders env) v')

87 _ -> tfail e

89 _ -> tfail e

88 where

90 where

@@ -143,7 +145,7 @@ match_unify ctxt env topx topy inj holes from =

143 let r = recoverable (normalise ctxt env x)

145 let r = recoverable (normalise ctxt env x)

144 (normalise ctxt env y)

146 (normalise ctxt env y)

145 let err = cantUnify from r

147 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

147 if (not r) then lift $ tfail err

149 if (not r) then lift $ tfail err

148 else do put (UI s ((x, y, True, env, err, from, Match) : f))

150 else do put (UI s ((x, y, True, env, err, from, Match) : f))

149 lift $ tfail err

151 lift $ tfail err

@@ -157,8 +159,9 @@ match_unify ctxt env topx topy inj holes from =

157 uB bnames x y = do UI s f <- get

159 uB bnames x y = do UI s f <- get

158 let r = recoverable (normalise ctxt env (binderTy x))

160 let r = recoverable (normalise ctxt env (binderTy x))

159 (normalise ctxt env (binderTy y))

161 (normalise ctxt env (binderTy y))

160− let err = cantUnify from r topx topy

162+ let err = cantUnify from r (topx, xfrom) (topy, yfrom)

163+ (CantUnify r (binderTy x, Nothing)

161− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

164+ (binderTy y, Nothing) (Msg "") (errEnv env) s)

162 (errEnv env) s

165 (errEnv env) s

163 put (UI s ((binderTy x, binderTy y,

166 put (UI s ((binderTy x, binderTy y,

164 False,

167 False,

@@ -179,7 +182,8 @@ match_unify ctxt env topx topy inj holes from =

179 let r = recoverable (normalise ctxt env x)

182 let r = recoverable (normalise ctxt env x)

180 (normalise ctxt env y)

183 (normalise ctxt env y)

181 let err = cantUnify from r

184 let err = cantUnify from r

185+ (topx, xfrom) (topy, yfrom)

182− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

186+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

183 put (UI s ((x, y, True, env, err, from, Match) : f))

187 put (UI s ((x, y, True, env, err, from, Match) : f))

184 lift $ tfail err

188 lift $ tfail err

185 combine bnames as [] = return as

189 combine bnames as [] = return as

@@ -241,7 +245,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

241 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

245 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

242 explicitHole t = t

246 explicitHole t = t

243

247

244−trimSolutions topx topy from env topns = followSols [] (dropPairs topns)

248+trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPairs topns)

245 where dropPairs [] = []

249 where dropPairs [] = []

246 dropPairs (n@(x, P _ x' _) : ns)

250 dropPairs (n@(x, P _ x' _) : ns)

247 | x == x' = dropPairs ns

251 | x == x' = dropPairs ns

@@ -258,7 +262,7 @@ trimSolutions topx topy from env topns = followSols [] (dropPairs topns)

258 = do vs' <- case t' of

262 = do vs' <- case t' of

259 P _ tn _ ->

263 P _ tn _ ->

260 if (n, tn) `elem` vs then -- cycle

264 if (n, tn) `elem` vs then -- cycle

261− tfail (cantUnify from False topx topy

265+ tfail (cantUnify from False (topx, xfrom) (topy, yfrom)

262 (Msg "") (errEnv env) 0)

266 (Msg "") (errEnv env) 0)

263 else return ((n, tn) : vs)

267 else return ((n, tn) : vs)

264 _ -> return vs

268 _ -> return vs

@@ -280,16 +284,18 @@ hasv (App f a) = hasv f || hasv a

280hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

284hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

281hasv _ = False

285hasv _ = False

282

286

283−unify :: Context -> Env -> TT Name -> TT Name ->

287+unify :: Context -> Env ->

288+ (TT Name, Maybe Provenance) ->

289+ (TT Name, Maybe Provenance) ->

284 [Name] -> [Name] -> [Name] -> [FailContext] ->

290 [Name] -> [Name] -> [Name] -> [FailContext] ->

285 TC ([(Name, TT Name)], Fails)

291 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 =

287-- traceWhen (hasv topx || hasv topy)

293-- traceWhen (hasv topx || hasv topy)

288-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

294-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

289 -- don't bother if topx and topy are different at the head

295 -- don't bother if topx and topy are different at the head

290 case runStateT (un False [] (renameBindersTm env topx)

296 case runStateT (un False [] (renameBindersTm env topx)

291 (renameBindersTm env topy)) (UI 0 []) of

297 (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

293 return (map (renameBinders env) v', [])

299 return (map (renameBinders env) v', [])

294 res ->

300 res ->

295 let topxn = renameBindersTm env (normalise ctxt env topx)

301 let topxn = renameBindersTm env (normalise ctxt env topx)

@@ -298,7 +304,7 @@ unify ctxt env topx topy inj holes usersupp from =

298 case runStateT (un False [] topxn topyn)

304 case runStateT (un False [] topxn topyn)

299 (UI 0 []) of

305 (UI 0 []) of

300 OK (v, UI _ fails) ->

306 OK (v, UI _ fails) ->

301− do v' <- trimSolutions topx topy from env v

307+ do v' <- trimSolutions (topx, xfrom) (topy, yfrom) from env v

302 return (map (renameBinders env) v', reverse fails)

308 return (map (renameBinders env) v', reverse fails)

303-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

309-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

304 Error e -> tfail e

310 Error e -> tfail e

@@ -470,7 +476,7 @@ unify ctxt env topx topy inj holes usersupp from =

470 let r = recoverable (normalise ctxt env x)

476 let r = recoverable (normalise ctxt env x)

471 (normalise ctxt env y)

477 (normalise ctxt env y)

472 let err = cantUnify from r

478 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

474 if (not r) then lift $ tfail err

480 if (not r) then lift $ tfail err

475 else do put (UI s ((x, y, True, env, err, from, Unify) : f))

481 else do put (UI s ((x, y, True, env, err, from, Unify) : f))

476 return [] -- lift $ tfail err

482 return [] -- lift $ tfail err

@@ -569,7 +575,8 @@ unify ctxt env topx topy inj holes usersupp from =

569 = do UI s f <- get

575 = do UI s f <- get

570 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

576 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

571 let err = cantUnify from r

577 let err = cantUnify from r

578+ (topx, xfrom) (topy, yfrom)

572− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

579+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

573 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

580 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

574 return []

581 return []

575

582

@@ -577,7 +584,8 @@ unify ctxt env topx topy inj holes usersupp from =

577 unifyFail x y = do UI s f <- get

584 unifyFail x y = do UI s f <- get

578 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

585 let r = recoverable (normalise ctxt env x) (normalise ctxt env y)

579 let err = cantUnify from r

586 let err = cantUnify from r

587+ (topx, xfrom) (topy, yfrom)

580− topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

588+ (CantUnify r (x, Nothing) (y, Nothing) (Msg "") (errEnv env) s) (errEnv env) s

581 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

589 put (UI s ((topx, topy, True, env, err, from, Unify) : f))

582 lift $ tfail err

590 lift $ tfail err

583

591

@@ -599,8 +607,8 @@ unify ctxt env topx topy inj holes usersupp from =

599 uB bnames x y = do UI s f <- get

607 uB bnames x y = do UI s f <- get

600 let r = recoverable (normalise ctxt env (binderTy x))

608 let r = recoverable (normalise ctxt env (binderTy x))

601 (normalise ctxt env (binderTy y))

609 (normalise ctxt env (binderTy y))

602− let err = cantUnify from r topx topy

610+ let err = cantUnify from r (topx, xfrom) (topy, yfrom)

603− (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

611+ (CantUnify r (binderTy x, Nothing) (binderTy y, Nothing) (Msg "") (errEnv env) s)

604 (errEnv env) s

612 (errEnv env) s

605 put (UI s ((binderTy x, binderTy y,

613 put (UI s ((binderTy x, binderTy y,

606 False,

614 False,

src/Idris/Delaborate.hs+2−2

@@ -199,7 +199,7 @@ pprintErr' i (InternalMsg s) =

199 text "This is probably a bug, or a missing error message.",

200 text ("Please consider reporting at " ++ bugaddr)

201 ]

202−pprintErr' i (CantUnify _ x_in y_in e sc s) =

202+pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

203 let (x_ns, y_ns, nms) = renameMNs x_in y_in

204 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in

205 text "Can't unify" <> indented (annTm x_ns

@@ -212,7 +212,7 @@ pprintErr' i (CantUnify _ x_in y_in e sc s) =

212 Msg "" -> empty

213 -- if the specific error is the same as the one we just printed,

214 -- 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

216 _ -> line <> line <> text "Specifically:" <>

217 indented (pprintErr' i e) <>

218 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

464 Error err -> if tcgen then return (recoverable ctxt err)

465 else return (validCase ctxt err ||

466 recoverable ctxt err)

467− where validCase ctxt (CantUnify _ topx topy e _ _)

467+ where validCase ctxt (CantUnify _ (topx, _) (topy, _) e _ _)

468 = let topx' = normalise ctxt [] topx

469 topy' = normalise ctxt [] topy in

470 not (sameFam topx' topy' || not (validCase ctxt e))

@@ -474,7 +474,7 @@ checkPossible info fc tcgen fname lhs_in

474 validCase ctxt (ElaboratingArg _ _ _ e) = validCase ctxt e

475 validCase ctxt _ = True

476

477− recoverable ctxt (CantUnify r topx topy e _ _)

477+ recoverable ctxt (CantUnify r (topx, _) (topy, _) e _ _)

478 = let topx' = normalise ctxt [] topx

479 topy' = normalise ctxt [] topy in

480 checkRec topx' topy'

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

704 OK (_, cs) -> do addConstraints fc cs

705 logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs

706 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))

708 i <- getIState

709 checkInferred fc (delab' i crhs True True) rhs

710 -- 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

81 -- Types must always convert

82 case converts ctxt [] clhs_ty crhs_ty of

83 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))

85 -- In safe mode, values must convert (Thinks: This is probably not

86 -- useful as is, perhaps it should require a proof of equality instead)

87 when safe $ case converts ctxt [] clhs_tm crhs_tm of

88 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))

91 case unApply (depat clhs_tm) of

92 (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

268 pimp (sUN "a") Placeholder True,

269 pexp ct])) True

270

271− forceErr env (CantUnify _ t t' _ _ _)

271+ forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

272 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

273 ht == txt "Lazy'" = True

274− forceErr env (CantUnify _ t t' _ _ _)

274+ forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

275 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

276 ht == txt "Lazy'" = True

277 forceErr env (InfiniteUnify _ t _)

@@ -2547,7 +2547,7 @@ reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT")

2547reflectErr :: Err -> Raw

2548reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]

2549reflectErr (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) =

2551 raw_apply (Var $ reflErrName "CantUnify")

2552 [ rawBool b

2553 , reflect t1

src/Idris/Prover.hs+1−1

@@ -83,7 +83,7 @@ prove opt ctxt lit n ty

83 "Expected type:" ++ show ty)

84 case converts ctxt [] ty pty of

85 OK _ -> return ()

86− Error e -> ierror (CantUnify False ty pty e [] 0)

86+ Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0)

87 ptm' <- applyOpts ptm

88 ei <- getErasureInfo `fmap` getIState

89 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)

969 = do (ltm, _) <- elabVal recinfo ERHS l

970 (rtm, _) <- elabVal recinfo ERHS r

971 ctxt <- getContext

972− case unify ctxt [] ltm rtm [] [] [] [] of

972+ case unify ctxt [] (ltm, Nothing) (rtm, Nothing) [] [] [] [] of

973 OK ans -> iputStrLn (show ans)

974 Error e -> iputStrLn (show e)

975

src/Idris/TypeSearch.hs+4−2

@@ -278,7 +278,7 @@ inArgTys = map . first . second

278

279typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]

280typeclassUnify 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 []

282 guard $ null (theHoles \\ map fst res)

283 let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs

284 return argTys'

@@ -424,7 +424,9 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

424 unifyQueue state [] = return state

425 unifyQueue state ((ty1, ty2) : queue) = do

426 --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) []

428 (state', queueAdditions) <- resolveUnis res state

430 (state', queueAdditions) <- resolveUnis res state

429 guard $ scoreCriterion (score state')

431 guard $ scoreCriterion (score state')

430 unifyQueue state' (queue ++ queueAdditions)

432 unifyQueue state' (queue ++ queueAdditions)