9596463 · Idris-dev · git.iko.soy

CHANGELOG+9

@@ -8,6 +8,9 @@ New in 0.9.17:

88* Quasiquotation supports the generation of Language.Reflection.Raw terms

99 in addition to Language.Reflection.TT. Types are used for disambiguation,

1010 defaulting to TT at the REPL.

11+* Language.Reflection.Quotable now takes an extra type parameter which

12+ determines the type to be quoted to. Instances are provided to quote

13+ common types to both TT and Raw.

1114* Library operators have been renamed for consistency with Haskell. In

1215 particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is

1316 now an alias for Functor.map. Correspondingly, ($>) and (<$) have

@@ -24,6 +27,12 @@ New in 0.9.17:

2427 called from foreign code

2528* Instances can now have documentation strings.

2629* Type providers can have documentation strings.

30+* Unification errors now (where possible) contain information about provenance

31+ of a type

32+* New REPL command ":core TM" that shows the elaborated form of TM along with

33+ its elaborated type using the syntax of TT. IDE mode has a corresponding

34+ command :elaborate-term for serialized terms.

35+

2736

2837New in 0.9.16:

2938--------------

libs/base/Data/Fin.idr+1−1

@@ -179,7 +179,7 @@ finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m))

179179 , TextPart "is less than", TermPart (getNat m)

180180 , TextPart "because", TermPart (P Bound n t)

181181 , TextPart "is a bound variable instead of a constant"

182− , TermPart (TConst (AType (ATInt ITBig)))

182+ , TermPart `(Integer : Type)

183183 ]

184184finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)

185185 = mkFinIntegerErr n m

libs/prelude/Language/Reflection/Tactical.idr+8

@@ -39,6 +39,8 @@ data Tactical : Type -> Type where

3939 prim__Claim : TTName -> Raw -> Tactical ()

4040 prim__Intro : Maybe TTName -> Tactical ()

4141

42+ prim__Debug : {a : Type} -> Maybe String -> Tactical a

43+

4244-------------

4345-- Public API

4446-------------

@@ -114,3 +116,9 @@ sourceLocation = do loc <- getSourceLocation

114116

115117rewriteWith : Raw -> Tactical ()

116118rewriteWith rule = prim__Rewrite rule

119+

120+debug : Tactical a

121+debug = prim__Debug Nothing

122+

123+debugMessage : String -> Tactical a

124+debugMessage msg = prim__Debug (Just msg)

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/AbsSyntaxTree.hs+1−6

@@ -347,6 +347,7 @@ data Command = Quit

347347 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.

348348 | Undefine [Name]

349349 | Check PTerm

350+ | Core PTerm

350351 | DocStr (Either Name Const) HowMuchDocs

351352 | TotCheck Name

352353 | Reload

@@ -1682,12 +1683,6 @@ isHoleName _ = False

16821683containsHole :: PTerm -> Bool

16831684containsHole pterm = or [isHoleName n | PRef _ n <- take 1000 $ universe pterm]

16841685

1685−-- | Pretty-printer helper for the binding site of a name

1686−bindingOf :: Name -- ^^ the bound name

1687− -> Bool -- ^^ whether the name is implicit

1688− -> Doc OutputAnnotation

1689−bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))

1690−

16911686-- | Pretty-printer helper for names that attaches the correct annotations

16921687prettyName

16931688 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator

src/Idris/Core/Binary.hs+28

@@ -23,6 +23,26 @@ instance Binary ErrorReportPart where

2323 3 -> fmap SubReport get

2424 _ -> error "Corrupted binary data for ErrorReportPart"

2525

26+instance Binary Provenance where

27+ put ExpectedType = putWord8 0

28+ put (SourceTerm t) = do putWord8 1

29+ put t

30+ put InferredVal = putWord8 2

31+ put GivenVal = putWord8 3

32+ put (TooManyArgs t) = do putWord8 4

33+ put t

34+

35+ get = do i <- getWord8

36+ case i of

37+ 0 -> return ExpectedType

38+ 1 -> do x1 <- get

39+ return (SourceTerm x1)

40+ 2 -> return InferredVal

41+ 3 -> return GivenVal

42+ 4 -> do x1 <- get

43+ return (TooManyArgs x1)

44+ _ -> error "Corrupted binary data for Provenance"

45+

2646instance Binary a => Binary (Err' a) where

2747 put (Msg str) = do putWord8 0

2848 put str

@@ -122,6 +142,10 @@ instance Binary a => Binary (Err' a) where

122142 put t

123143 put (CantMatch t) = do putWord8 35

124144 put t

145+ put (ElabDebug x1 x2 x3) = do putWord8 36

146+ put x1

147+ put x2

148+ put x3

125149

126150 get = do i <- getWord8

127151 case i of

@@ -177,6 +201,10 @@ instance Binary a => Binary (Err' a) where

177201 return $ ReflectionFailed x y

178202 34 -> fmap WithFnType get

179203 35 -> fmap CantMatch get

204+ 36 -> do x1 <- get

205+ x2 <- get

206+ x3 <- get

207+ return (ElabDebug x1 x2 x3)

180208 _ -> error "Corrupted binary data for Err'"

181209----- Generated by 'derive'

182210

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

@@ -8,6 +8,7 @@ import Control.Applicative

88import Control.Arrow

99import Control.Monad.RWS

1010import Control.Monad.State

11+import qualified Data.Set as S

1112import Data.List

1213import Data.Maybe

1314import qualified Data.Map.Strict as M

@@ -19,7 +20,7 @@ ucheck :: [(UConstraint, FC)] -> TC ()

1920ucheck cs = acyclic rels (map fst (M.toList rels))

2021 where lhs (ULT l _) = l

2122 lhs (ULE l _) = l

22− cs' = nub cs

23+ cs' = S.toList (S.fromList cs)

2324 rels = mkRels cs' M.empty

2425

2526type Relations = M.Map UExp [(UConstraint, FC)]

src/Idris/Core/DeepSeq.hs+8

@@ -43,6 +43,13 @@ instance NFData Raw where

4343instance NFData FC where

4444 rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

4545

46+instance NFData Provenance where

47+ rnf ExpectedType = ()

48+ rnf InferredVal = ()

49+ rnf GivenVal = ()

50+ rnf (SourceTerm x1) = rnf x1 `seq` ()

51+ rnf (TooManyArgs x1) = rnf x1 `seq` ()

52+

4653instance NFData Err where

4754 rnf (Msg x1) = rnf x1 `seq` ()

4855 rnf (InternalMsg x1) = rnf x1 `seq` ()

@@ -88,6 +95,7 @@ instance NFData Err where

8895 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

8996 rnf (ProviderError x1) = rnf x1 `seq` ()

9097 rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

98+ rnf (ElabDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

9199

92100instance NFData ImplicitInfo where

93101 rnf (Impl x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+17−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

@@ -778,6 +779,7 @@ try' t1 t2 proofSearch

778779 recoverableErr (ProofSearchFail _) = False

779780 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

780781 recoverableErr (At _ e) = recoverableErr e

782+ recoverableErr (ElabDebug _ _ _) = False

781783 recoverableErr _ = True

782784

783785tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

@@ -839,6 +841,19 @@ prunStateT pmax zok ps x s

839841 else OK ((v, newpmax, problems p), s')

840842 Error e -> Error e

841843

844+debugElaborator :: Maybe String -> Elab' aux a

845+debugElaborator msg = do ps <- fmap proof get

846+ saveState -- so we don't need to remember the hole order

847+ hs <- get_holes

848+ holeInfo <- mapM getHoleInfo hs

849+ loadState

850+ lift . Error $ ElabDebug msg (getProofTerm (pterm ps)) holeInfo

851+ where getHoleInfo :: Name -> Elab' aux (Name, Type, [(Name, Binder Type)])

852+ getHoleInfo h = do focus h

853+ g <- goal

854+ env <- get_env

855+ return (h, g, env)

856+

842857qshow :: Fails -> String

843858qshow fs = show (map (\ (x, y, _, _, _, _, _) -> (x, y)) fs)

844859

src/Idris/Core/Evaluate.hs+6−3

@@ -9,7 +9,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

1111 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

12− lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

12+ lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

1313 mapDefCtxt,

1414 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

1515 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

@@ -1007,7 +1007,10 @@ isTCDict n ctxt

10071007 _ -> False

10081008

10091009lookupP :: Name -> Context -> [Term]

1010−lookupP n ctxt

1010+lookupP = lookupP_all False

1011+

1012+lookupP_all :: Bool -> Name -> Context -> [Term]

1013+lookupP_all all n ctxt

10111014 = do def <- lookupCtxt n (definitions ctxt)

10121015 p <- case def of

10131016 (Function ty tm, a, _, _) -> return (P Ref n ty, a)

@@ -1015,7 +1018,7 @@ lookupP n ctxt

10151018 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

10161019 (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

10171020 case snd p of

1018− Hidden -> []

1021+ Hidden -> if all then return (fst p) else []

10191022 _ -> return (fst p)

10201023

10211024lookupDefExact :: Name -> Context -> Maybe Def

src/Idris/Core/ProofState.hs+46−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,12 +477,20 @@ 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, Just $ SourceTerm val)

481+ (ty, Just (chkPurpose val ty))

477482 ps <- get

478483 let (uh, uns) = unified ps

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

480485-- addLog (show (uh, uns ++ ns))

481486 return $ Bind x (Guess ty val) sc

487+ where

488+ -- some expected types show up commonly in errors and indicate a

489+ -- specific problem.

490+ -- argTy -> retTy suggests a function applied to too many arguments

491+ chkPurpose val (Bind _ (Pi _ (P _ (MN _ _) _) _) (P _ (MN _ _) _))

492+ = TooManyArgs val

493+ chkPurpose _ _ = ExpectedType

482494fill _ _ _ _ = fail "Can't fill here."

483495

484496-- As fill, but attempts to solve other goals by matching

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

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

489501-- let valtyn = normalise ctxt env valty

490502-- let tyn = normalise ctxt env ty

491− ns <- match_unify' ctxt env valty ty

503+ ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)

504+ (ty, Just ExpectedType)

492505 ps <- get

493506 let (uh, uns) = unified ps

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

@@ -506,7 +519,8 @@ complete_fill :: RunTactic

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

507520 do let guess = forget val

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

509− ns <- unify' ctxt env valty ty

522+ ns <- unify' ctxt env (valty, Just $ SourceTerm val')

523+ (ty, Just ExpectedType)

510524 ps <- get

511525 let (uh, uns) = unified ps

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

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

524538 dropdots <-

525539 case lookup x (notunified ps) of

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

527− do match_unify' ctxt env tm val

541+ do match_unify' ctxt env (tm, Just InferredVal)

542+ (val, Just GivenVal)

528543 return [x]

529544 _ -> return []

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

@@ -567,7 +582,7 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

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

568583 case t' of

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

570− do ns <- unify' ctxt env s tyv

585+ do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)

571586 ps <- get

572587 let (uh, uns) = unified ps

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

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

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

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

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

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

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

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

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

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

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

600615

@@ -817,13 +832,17 @@ updateEnv ns [] = []

817832updateEnv ns ((n, b) : env)

818833 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

819834

835+updateProv ns (SourceTerm t) = SourceTerm $ updateSolvedTerm ns t

836+updateProv ns p = p

837+

820838updateError [] err = err

821839updateError ns (At f e) = At f (updateError ns e)

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

823841updateError ns (ElaboratingArg f a env e)

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

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

844+ = CantUnify b (updateSolvedTerm ns l, fmap (updateProv ns) lp)

845+ (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc

827846updateError ns e = e

828847

829848solveInProblems x val [] = []

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

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

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

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

840− ((t,t',True, env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

859+ ((t,t',True, env,CantUnify True (t, Nothing) (t', Nothing) (Msg "") [] 0, [],Match) : ps_acc)

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

842861

843862updateNotunified [] nu = nu

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

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

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

848867

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

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

870+getProvenance _ = (Nothing, Nothing)

871+

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

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

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

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

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

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

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

886+ (lp, rp) = getProvenance err

863887 err' = updateError ns err

864888 env' = updateEnv ns env in

865889 if newx || newy || ready ||

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

867− case unify ctxt env' x' y' inj hs usupp while of

891+ case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of

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

869893 up (ns ++ v) ps

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

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

887911 | all || um == Match =

888912 let x' = updateSolvedTerm ns x

889913 y' = updateSolvedTerm ns y

914+ (lp, rp) = getProvenance err

890915 err' = updateError ns err

891916 env' = updateEnv ns env in

892− case match_unify ctxt env' x' y' inj hs while of

917+ case match_unify ctxt env' (x', lp) (y', rp) inj hs while of

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

894919 up (ns ++ v) ps

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

src/Idris/Core/TT.hs+117−6

@@ -30,7 +30,7 @@ import Data.Char

3030import Data.Data (Data)

3131import Numeric (showIntAtBase)

3232import qualified Data.Text as T

33−import Data.List hiding (insert)

33+import Data.List hiding (group, insert)

3434import Data.Set(Set, member, fromList, insert)

3535import Data.Maybe (listToMaybe)

3636import Data.Foldable (Foldable)

@@ -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,25 @@ data ErrorReportPart = TextPart String

120120-- Please remember to keep Err synchronised with

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

122122

123+data Provenance = ExpectedType

124+ | TooManyArgs Term

125+ | InferredVal

126+ | GivenVal

127+ | SourceTerm Term

128+ deriving (Show, Eq, Data, Typeable)

129+{-!

130+deriving instance NFData Err

131+deriving instance Binary Err

132+!-}

133+

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

124135-- if they reach the top level.

125136data Err' t

126137 = Msg String

127138 | InternalMsg String

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

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

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

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

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

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

131144 -- unification succeed

@@ -162,6 +175,8 @@ data Err' t

162175 | LoadingFailed String (Err' t)

163176 | ReflectionError [[ErrorReportPart]] (Err' t)

164177 | ReflectionFailed String (Err' t)

178+ | ElabDebug (Maybe String) t [(Name, t, [(Name, Binder t)])]

179+ -- ^ User-specified message, proof term, goals with context (first goal is focused)

165180 deriving (Eq, Functor, Data, Typeable)

166181

167182type Err = Err' Term

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

209224instance Sized Err where

210225 size (Msg msg) = length msg

211226 size (InternalMsg msg) = length msg

212− size (CantUnify _ left right err _ score) = size left + size right + size err

227+ size (CantUnify _ left right err _ score) = size (fst left) + size (fst right) + size err

213228 size (InfiniteUnify _ right _) = size right

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

215230 size (UnifyScope _ _ right _) = size right

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

261276

262277instance Pretty Err OutputAnnotation where

263278 pretty (Msg m) = text m

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

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

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

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

267282 pretty (ProviderError msg) = text msg

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

781796-- | Universe constraints

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

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

784− deriving Eq

799+ deriving (Eq, Ord)

785800

786801instance Show UConstraint where

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

@@ -1496,3 +1511,99 @@ allTTNames = nub . allNamesIn

14961511 nb t = allNamesIn (binderTy t)

14971512 allNamesIn (App f a) = allNamesIn f ++ allNamesIn a

14981513 allNamesIn _ = []

1514+

1515+

1516+-- | Pretty-print a term

1517+pprintTT :: [Name] -- ^ The bound names (for highlighting and de Bruijn indices)

1518+ -> TT Name -- ^ The term to be printed

1519+ -> Doc OutputAnnotation

1520+pprintTT bound tm = pp startPrec bound tm

1521+

1522+ where

1523+ startPrec = 0

1524+ appPrec = 10

1525+

1526+ pp p bound (P Bound n ty) = annotate (AnnBoundName n False) (text $ show n)

1527+ pp p bound (P nt n ty) = annotate (AnnName n Nothing Nothing Nothing)

1528+ (text $ show n)

1529+ pp p bound (V i)

1530+ | i < length bound = let n = bound !! i

1531+ in annotate (AnnBoundName n False) (text $ show n)

1532+ | otherwise = text ("{{{V" ++ show i ++ "}}}")

1533+ pp p bound (Bind n b sc) = ppb p bound n b $

1534+ pp startPrec (n:bound) sc

1535+ pp p bound (App tm1 tm2) =

1536+ bracket p appPrec . group . hang 2 $

1537+ pp appPrec bound tm1 <> line <>

1538+ pp (appPrec + 1) bound tm2

1539+ pp p bound (Constant c) = annotate (AnnConst c) (text (show c))

1540+ pp p bound (Proj tm i) =

1541+ lparen <> pp startPrec bound tm <> rparen <>

1542+ text "!" <> text (show i)

1543+ pp p bound Erased = text "<<<erased>>>"

1544+ pp p bound Impossible = text "<<<impossible>>>"

1545+ pp p bound (TType ue) = annotate (AnnType "Type" "The type of types") $

1546+ text "Type"

1547+ pp p bound (UType u) = text (show u)

1548+

1549+ ppb p bound n (Lam ty) sc =

1550+ bracket p startPrec . group . align . hang 2 $

1551+ text "λ" <+> bindingOf n False <+> text "." <> line <> sc

1552+ ppb p bound n (Pi _ ty k) sc =

1553+ bracket p startPrec . group . align $

1554+ lparen <> (bindingOf n False) <+> colon <+>

1555+ (group . align) (pp startPrec bound ty) <>

1556+ rparen <+> mkArrow k <> line <> sc

1557+ where mkArrow (UType UniqueType) = text "⇴"

1558+ mkArrow (UType NullType) = text "⥛"

1559+ mkArrow _ = text "→"

1560+ ppb p bound n (Let ty val) sc =

1561+ bracket p startPrec . group . align $

1562+ (group . hang 2) (annotate AnnKeyword (text "let") <+>

1563+ bindingOf n False <+> colon <+>

1564+ pp startPrec bound ty <+>

1565+ text "=" <> line <>

1566+ pp startPrec bound val) <> line <>

1567+ (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)

1568+ ppb p bound n (NLet ty val) sc =

1569+ bracket p startPrec . group . align $

1570+ (group . hang 2) (annotate AnnKeyword (text "nlet") <+>

1571+ bindingOf n False <+> colon <+>

1572+ pp startPrec bound ty <+>

1573+ text "=" <> line <>

1574+ pp startPrec bound val) <> line <>

1575+ (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)

1576+ ppb p bound n (Hole ty) sc =

1577+ bracket p startPrec . group . align . hang 2 $

1578+ text "?" <+> bindingOf n False <+> text "." <> line <> sc

1579+ ppb p bound n (GHole _ ty) sc =

1580+ bracket p startPrec . group . align . hang 2 $

1581+ text "¿" <+> bindingOf n False <+> text "." <> line <> sc

1582+ ppb p bound n (Guess ty val) sc =

1583+ bracket p startPrec . group . align . hang 2 $

1584+ text "?" <> bindingOf n False <+>

1585+ text "≈" <+> pp startPrec bound val <+>

1586+ text "." <> line <> sc

1587+ ppb p bound n (PVar ty) sc =

1588+ bracket p startPrec . group . align . hang 2 $

1589+ annotate AnnKeyword (text "pat") <+>

1590+ bindingOf n False <+> colon <+> pp startPrec bound ty <+>

1591+ text "." <> line <>

1592+ sc

1593+ ppb p bound n (PVTy ty) sc =

1594+ bracket p startPrec . group . align . hang 2 $

1595+ annotate AnnKeyword (text "patTy") <+>

1596+ bindingOf n False <+> colon <+> pp startPrec bound ty <+>

1597+ text "." <> line <>

1598+ sc

1599+

1600+ bracket outer inner doc

1601+ | outer > inner = lparen <> doc <> rparen

1602+ | otherwise = doc

1603+

1604+

1605+-- | Pretty-printer helper for the binding site of a name

1606+bindingOf :: Name -- ^^ the bound name

1607+ -> Bool -- ^^ whether the name is implicit

1608+ -> Doc OutputAnnotation

1609+bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))

src/Idris/Core/Typecheck.hs+4−1

@@ -81,7 +81,10 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

8181 Env -> Raw -> StateT UCs TC (Term, Type)

8282 chk u env (Var n)

8383 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

84− | (P nt n' ty : _) <- lookupP n ctxt = return (P nt n' ty, ty)

84+ -- If we're elaborating, we don't want the private names; if we're

85+ -- checking an already elaborated term, we do

86+ | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt

87+ = return (P nt n' ty, ty)

8588 | otherwise = do lift $ tfail $ NoSuchVariable n

8689 chk u env ap@(RApp f a)

8790 = do (fv, fty) <- chk u env f

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

@@ -1,4 +1,5 @@

11{-# LANGUAGE PatternGuards #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

23module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr) where

34

45-- Convert core TT back into high level syntax, primarily for display

@@ -32,6 +33,7 @@ delabTy i n

3233 (ty:_) -> case lookupCtxt n (idris_implicits i) of

3334 (imps:_) -> delabTy' i imps ty False False

3435 _ -> delabTy' i [] ty False False

36+ [] -> error "delabTy: got non-existing name"

3537

3638delab' :: IState -> Term -> Bool -> Bool -> PTerm

3739delab' i t f mvs = delabTy' i [] t f mvs

@@ -86,6 +88,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

8688 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

8789 de env plic (Bind n bb sc) = de ((n,n):env) [] sc

8890 de env _ (Constant i) = PConstant i

91+ de env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"

8992 de env _ Erased = Placeholder

9093 de env _ Impossible = Placeholder

9194 de env _ (TType i) = PType

@@ -183,6 +186,7 @@ pprintDelabTy i n

183186 case lookupCtxt n (idris_implicits i) of

184187 (imps:_) -> delabTy' i imps ty False False

185188 _ -> delabTy' i [] ty False False

189+ [] -> error "pprintDelabTy got a name that doesn't exist"

186190

187191pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

188192pprintTerm ist = pprintTerm' ist []

@@ -190,6 +194,20 @@ pprintTerm ist = pprintTerm' ist []

190194pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

191195pprintTerm' ist bnd tm = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) tm

192196

197+pprintProv :: IState -> [(Name, Term)] -> Provenance -> Doc OutputAnnotation

198+pprintProv i e ExpectedType = text "Expected type"

199+pprintProv i e InferredVal = text "Inferred value"

200+pprintProv i e GivenVal = text "Given value"

201+pprintProv i e (SourceTerm tm)

202+ = text "Type of " <>

203+ annotate (AnnTerm (zip (map fst e) (repeat False)) tm)

204+ (pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm))

205+pprintProv i e (TooManyArgs tm)

206+ = text "Is " <>

207+ annotate (AnnTerm (zip (map fst e) (repeat False)) tm)

208+ (pprintTerm' i (zip (map fst e) (repeat False)) (delab i tm))

209+ <> text " applied to too many arguments?"

210+

193211pprintErr :: IState -> Err -> Doc OutputAnnotation

194212pprintErr i err = pprintErr' i (fmap (errReverse i) err)

195213

@@ -199,20 +217,28 @@ pprintErr' i (InternalMsg s) =

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

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

201219 ]

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

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

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

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

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

206224 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

207− ++ zip nms (repeat False)) x)) <$>

225+ ++ zip nms (repeat False)) x))

226+ <> case xprov of

227+ Nothing -> empty

228+ Just t -> text " (" <> pprintProv i sc t <> text ")"

229+ <$>

208230 text "with" <> indented (annTm y_ns

209231 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

210− ++ zip nms (repeat False)) y)) <>

232+ ++ zip nms (repeat False)) y))

233+ <> case yprov of

234+ Nothing -> empty

235+ Just t -> text " (" <> pprintProv i sc t <> text ")"

236+ <>

211237 case e of

212238 Msg "" -> empty

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

214240 -- there's no need to print it

215− CantUnify _ x_in' y_in' _ _ _ | x_in == x_in' && y_in == y_in' -> empty

241+ CantUnify _ (x_in', _) (y_in',_) _ _ _ | x_in == x_in' && y_in == y_in' -> empty

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

217243 indented (pprintErr' i e) <>

218244 if (opt_errContext (idris_options i)) then showSc i sc else empty

@@ -335,10 +361,30 @@ pprintErr' i (ReflectionFailed msg err) =

335361 text "When attempting to perform error reflection, the following internal error occurred:" <>

336362 indented (pprintErr' i err) <>

337363 text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)

338−

339−-- Make sure the machine invented names are shown helpfully to the user, so

364+pprintErr' i (ElabDebug msg tm holes) =

365+ text "Elaboration halted." <>

366+ maybe empty (indented . text) msg <> line <>

367+ text "Term: " <> indented (pprintTT [] tm) <> line <>

368+ text "Holes:" <>

369+ indented (vsep (map ppHole holes))

370+

371+ where ppHole :: (Name, Type, Env) -> Doc OutputAnnotation

372+ ppHole (hn, goal, env) =

373+ ppAssumptions [] (reverse env) <>

374+ text "----------------------------------" <> line <>

375+ bindingOf hn False <+> text ":" <+>

376+ pprintTT (map fst (reverse env)) goal <> line

377+ ppAssumptions :: [Name] -> Env -> Doc OutputAnnotation

378+ ppAssumptions ns [] = empty

379+ ppAssumptions ns ((n, b) : rest) =

380+ bindingOf n False <+>

381+ text ":" <+>

382+ pprintTT ns (binderTy b) <>

383+ line <>

384+ ppAssumptions (n:ns) rest

385+

386+-- | Make sure the machine invented names are shown helpfully to the user, so

340387-- that any names which differ internally also differ visibly

341−

342388renameMNs :: Term -> Term -> (Term, Term, [Name])

343389renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

344390 newnames = evalState (getRenames [] ns) 1 in

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+9−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 _)

@@ -1596,6 +1596,12 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

15961596 Just name -> fmap Just $ reifyTTName name

15971597 intro n

15981598 returnUnit

1599+ | n == tacN "prim__Debug", [ty, msg] <- args

1600+ = do let msg' = fromTTMaybe msg

1601+ case msg' of

1602+ Nothing -> debugElaborator Nothing

1603+ Just (Constant (Str m)) -> debugElaborator (Just m)

1604+ Just x -> lift . tfail . InternalMsg $ "Can't reify message for debugging: " ++ show x

15991605 runTacTm x = lift . tfail . InternalMsg $ "tactical is not implemented for " ++ show x

16001606

16011607-- Running tactics directly

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

25472553reflectErr :: Err -> Raw

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

25492555reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]

2550−reflectErr (CantUnify b t1 t2 e ctxt i) =

2556+reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =

25512557 raw_apply (Var $ reflErrName "CantUnify")

25522558 [ rawBool b

25532559 , reflect t1

src/Idris/IdeMode.hs+3

@@ -229,6 +229,7 @@ data IdeModeCommand = REPLCompletions String

229229 | TermNormalise [(Name, Bool)] Term

230230 | TermShowImplicits [(Name, Bool)] Term

231231 | TermNoImplicits [(Name, Bool)] Term

232+ | TermElab [(Name, Bool)] Term

232233 | PrintDef String

233234 | ErrString Err

234235 | ErrPPrint Err

@@ -278,6 +279,8 @@ sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded])

278279 Just (TermShowImplicits bnd tm)

279280sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

280281 Just (TermNoImplicits bnd tm)

282+sexpToCommand (SexpList [SymbolAtom "elaborate-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

283+ Just (TermElab bnd tm)

281284sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)

282285sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded

283286sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded

src/Idris/Output.hs+1−1

@@ -61,7 +61,7 @@ iRender d = do w <- getWidth

6161 if n < 1

6262 then renderPretty 1.0 1000000000 d

6363 else renderPretty 0.8 n d

64− AutomaticWidth | ideMode -> return $ renderPretty 1.0 1000000000 d

64+ AutomaticWidth | ideMode -> return $ renderPretty 1.0 80 d

6565 | otherwise -> do width <- runIO getScreenWidth

6666 return $ renderPretty 0.8 width d

6767

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+15−1

@@ -494,6 +494,15 @@ runIdeModeCommand h id orig fn modes (IdeMode.TermShowImplicits bnd tm) =

494494 ideModeForceTermImplicits h id bnd True tm

495495runIdeModeCommand h id orig fn modes (IdeMode.TermNoImplicits bnd tm) =

496496 ideModeForceTermImplicits h id bnd False tm

497+runIdeModeCommand h id orig fn modes (IdeMode.TermElab bnd tm) =

498+ do ist <- getIState

499+ let ptm = annotate (AnnTerm bnd tm)

500+ (pprintTT (map fst bnd) tm)

501+ msg = (IdeMode.SymbolAtom "ok",

502+ displaySpans .

503+ renderPretty 0.9 70 .

504+ fmap (fancifyAnnots ist) $ ptm)

505+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

497506runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) =

498507 case splitName name of

499508 Left err -> iPrintError err

@@ -556,6 +565,7 @@ idemodeProcess fn (Undefine n) = process fn (Undefine n)

556565idemodeProcess fn (ExecVal t) = process fn (ExecVal t)

557566idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

558567idemodeProcess fn (Check t) = process fn (Check t)

568+idemodeProcess fn (Core t) = process fn (Core t)

559569idemodeProcess fn (DocStr n w) = process fn (DocStr n w)

560570idemodeProcess fn Universes = process fn Universes

561571idemodeProcess fn (Defn n) = do process fn (Defn n)

@@ -908,6 +918,10 @@ process fn (Check t)

908918 _ -> iPrintTermWithType (pprintDelab ist tm)

909919 (pprintDelab ist ty)

910920

921+process fn (Core t)

922+ = do (tm, ty) <- elabVal recinfo ERHS t

923+ iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)

924+

911925process fn (DocStr (Left n) w)

912926 = do ist <- getIState

913927 let docs = lookupCtxtName n (idris_docstrings ist) ++

@@ -969,7 +983,7 @@ process fn (DebugUnify l r)

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

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

971985 ctxt <- getContext

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

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

973987 OK ans -> iputStrLn (show ans)

974988 Error e -> iputStrLn (show e)

975989

src/Idris/REPLParser.hs+1

@@ -41,6 +41,7 @@ allHelp = [ (map (':' :) names, args, text)

4141parserCommandsForHelp :: CommandTable

4242parserCommandsForHelp =

4343 [ exprArgCmd ["t", "type"] Check "Check the type of an expression"

44+ , exprArgCmd ["core"] Core "View the core language representation of a term"

4445 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"

4546 , (["doc"], NameArg, "Show internal documentation", cmd_doc)

4647 , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"

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)

test/basic006/expected+2−2

@@ -1,8 +1,8 @@

11test020a.idr:16:18:When elaborating right hand side of foo:

22When elaborating an application of function Prelude.List.reverse:

33 Can't unify

4− Vect n a

4+ Vect n a (Type of xs)

55 with

6− List a

6+ List a (Expected type)

77[3, 2, 1]

88"Number 42"

test/proof002/expected+2−2

@@ -1,9 +1,9 @@

11Reflect.idr:208:38:When elaborating right hand side of testReflect1:

22When elaborating an application of function Reflect.getJust:

33 Can't unify

4− IsJust (Just x1)

4+ IsJust (Just x1) (Type of ItIsJust)

55 with

6− IsJust (prove (getProof x))

6+ IsJust (prove (getProof x)) (Expected type)

77

88 Specifically:

99 Can't unify

test/reg007/expected+2−2

@@ -1,9 +1,9 @@

11reg007.lidr:8:1:A.n is already defined

22reg007.lidr:12:11:When elaborating right hand side of hurrah:

33Can't unify

4− n = lala

4+ n = lala (Type of isSame)

55with

6− 0 = 1

6+ 0 = 1 (Expected type)

77

88Specifically:

99 Can't unify

test/reg023/expected+2−2

@@ -1,5 +1,5 @@

11reg023.idr:7:5:When elaborating right hand side of bad:

22Can't unify

3− [94mNat[0m

3+ [94mNat[0m (Type of [91m0[0m)

44with

5− [92mf[0m [94mNat[0m

5+ [92mf[0m [94mNat[0m (Expected type)

test/reg044/expected+2−2

@@ -1,8 +1,8 @@

11reg044.idr:4:4:When elaborating right hand side of Main.pf:

22Can't unify

3− [95mb[0m [94m=[0m [95mb[0m

3+ [95mb[0m [94m=[0m [95mb[0m (Type of [91mRefl[0m)

44with

5− [95ma[0m [94m=[0m [95mb[0m

5+ [95ma[0m [94m=[0m [95mb[0m (Expected type)

66

77Specifically:

88 Can't unify

test/tutorial006/expected+4−4

@@ -1,9 +1,9 @@

11tutorial006a.idr:5:23:When elaborating right hand side of vapp:

22When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::[0m:

33 Can't unify

4− [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m

4+ [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m (Type of vapp [95mxs[0m [95mxs[0m)

55 with

6− [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m

6+ [94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m (Expected type)

77

88 Specifically:

99 Can't unify

@@ -12,9 +12,9 @@ When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::

1212 [92mplus[0m [95mn[0m [95mm[0m

1313tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity:

1414Can't unify

15− [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m))

15+ [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)) (Type of [91meven[0m)

1616with

17− [94mParity[0m ([91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m)))

17+ [94mParity[0m ([91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))) (Expected type)

1818

1919Specifically:

2020 Can't unify