fdfa04c · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Utils.idr+4−4

@@ -122,13 +122,13 @@ mutual

122122 _ == _ = False

123123

124124implementation Show TTUExp where

125− showPrec d (UVar i) = showCon d "UVar" $ showArg i

125+ showPrec d (UVar ns i) = showCon d "UVar" $ showArg ns ++ showArg i

126126 showPrec d (UVal i) = showCon d "UVal" $ showArg i

127127

128128implementation Eq TTUExp where

129− (UVar i) == (UVar j) = i == j

130− (UVal i) == (UVal j) = i == j

131− x == y = False

129+ (UVar nsi i) == (UVar nsj j) = nsi == nsj && i == j

130+ (UVal i) == (UVal j) = i == j

131+ x == y = False

132132

133133implementation Show NativeTy where

134134 show IT8 = "IT8"

libs/prelude/Language/Reflection.idr+3−3

@@ -573,7 +573,7 @@ implementation DecEq SpecialName where

573573

574574data TTUExp =

575575 ||| Universe variable

576− UVar Int |

576+ UVar String Int |

577577 ||| Explicit universe level

578578 UVal Int

579579%name TTUExp uexp

@@ -1026,12 +1026,12 @@ mutual

10261026

10271027implementation Quotable TTUExp TT where

10281028 quotedTy = `(TTUExp)

1029− quote (UVar x) = `(UVar ~(quote x))

1029+ quote (UVar ns x) = `(UVar ~(quote ns) ~(quote x))

10301030 quote (UVal x) = `(UVal ~(quote x))

10311031

10321032implementation Quotable TTUExp Raw where

10331033 quotedTy = `(TTUExp)

1034− quote (UVar x) = `(UVar ~(quote {t=Raw} x))

1034+ quote (UVar ns x) = `(UVar ~(quote ns) ~(quote {t=Raw} x))

10351035 quote (UVal x) = `(UVal ~(quote {t=Raw} x))

10361036

10371037implementation Quotable NativeTy TT where

src/Idris/AbsSyntax.hs+2

@@ -700,6 +700,8 @@ addConstraints fc (v, cs)

700700 putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

701701 where

702702 insertAll [] c = c

703+ insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics

704+ insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics

703705 insertAll ((c, fc) : cs) ics

704706 = insertAll cs $ S.insert (ConstraintFC c fc) ics

705707

src/Idris/AbsSyntaxTree.hs+15−9

@@ -65,8 +65,9 @@ data ElabInfo = EInfo {

6565 params :: [(Name, PTerm)]

6666 , inblock :: Ctxt [Name] -- ^ names in the block, and their params

6767 , liftname :: Name -> Name

68− , namespace :: Maybe [String]

68+ , namespace :: [String]

6969 , elabFC :: Maybe FC

70+ , constraintNS :: String -- ^ filename for adding to constraint variables

7071 , pe_depth :: Int

7172

7273 -- | We may, recursively, collect transformations to do on the rhs,

@@ -76,7 +77,10 @@ data ElabInfo = EInfo {

7677 }

7778

7879toplevel :: ElabInfo

79−toplevel = EInfo [] emptyContext id Nothing Nothing 0 id (\_ _ _ -> fail "Not implemented")

80+toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 id (\_ _ _ -> fail "Not implemented")

81+

82+toplevelWith :: String -> ElabInfo

83+toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 id (\_ _ _ -> fail "Not implemented")

8084

8185eInfoNames :: ElabInfo -> [Name]

8286eInfoNames info = map fst (params info) ++ M.keys (inblock info)

@@ -378,6 +382,7 @@ data IBCWrite = IBCFix FixDecl

378382 | IBCAutoHint Name Name

379383 | IBCDeprecate Name String

380384 | IBCFragile Name String

385+ | IBCConstraint FC UConstraint

381386 deriving Show

382387

383388-- | The initial state for the compiler

@@ -1668,13 +1673,14 @@ expandNS syn n = case syn_namespace syn of

16681673-- For inferring types of things

16691674

16701675bi = fileFC "builtin"

1676+primfc = fileFC "(primitive)"

16711677

16721678inferTy = sMN 0 "__Infer"

16731679inferCon = sMN 0 "__infer"

1674−inferDecl = PDatadecl inferTy NoFC

1680+inferDecl = PDatadecl inferTy primfc

16751681 (PType bi)

1676− [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (

1677− PPi expl (sMN 0 "ival") NoFC (PRef bi [] (sMN 0 "iType"))

1682+ [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (

1683+ PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))

16781684 (PRef bi [] inferTy)), bi, [])]

16791685inferOpts = []

16801686

@@ -1687,7 +1693,7 @@ getInferTerm (App _ (App _ _ _) tm) = tm

16871693getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

16881694

16891695getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

1690− where toTy (Lam t) = Pi Nothing t (TType (UVar 0))

1696+ where toTy (Lam t) = Pi Nothing t (TType (UVar [] 0))

16911697 toTy (PVar t) = PVTy t

16921698 toTy b = b

16931699getInferType (App _ (App _ _ ty) _) = ty

@@ -1728,12 +1734,12 @@ eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $

17281734 "\n\n" ++

17291735 "You may need to use `(~=~)` to explicitly request heterogeneous equality."

17301736

1731−eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]

1737+eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]

17321738 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]

17331739 (PType bi)))

17341740 [(reflDoc, reflParamDoc,

1735− eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (

1736− PPi impl (n "x") NoFC (PRef bi [] (n "A"))

1741+ eqCon, primfc, PPi impl (n "A") primfc (PType bi) (

1742+ PPi impl (n "x") primfc (PRef bi [] (n "A"))

17371743 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,

17381744 pimp (n "B") Placeholder False,

17391745 pexp (PRef bi [] (n "x")),

src/Idris/CaseSplit.hs+2−2

@@ -68,7 +68,7 @@ split n t'

6868 mapM_ (\n -> setAccessibility n Public) (allNamesIn t')

6969 -- ETyDecl rather then ELHS because there'll be explicit type

7070 -- matching

71− (tm, ty, pats) <- elabValBind recinfo ETyDecl True (addImplPat ist t')

71+ (tm, ty, pats) <- elabValBind (recinfo (fileFC "casesplit")) ETyDecl True (addImplPat ist t')

7272 -- ASSUMPTION: tm is in normal form after elabValBind, so we don't

7373 -- need to do anything special to find out what family each argument

7474 -- is in

@@ -242,7 +242,7 @@ tidy ist tm ty = return tm

242242-- tidyVar t = t

243243

244244elabNewPat :: PTerm -> Idris (Bool, PTerm)

245−elabNewPat t = idrisCatch (do (tm, ty) <- elabVal recinfo ELHS t

245+elabNewPat t = idrisCatch (do (tm, ty) <- elabVal (recinfo (fileFC "casesplit")) ELHS t

246246 i <- getIState

247247 return (True, delab i tm))

248248 (\e -> do i <- getIState

src/Idris/Core/Binary.hs+5−3

@@ -592,15 +592,17 @@ instance Binary NameType where

592592-- record concrete levels only, for now

593593instance Binary UExp where

594594 put x = case x of

595− UVar t -> do putWord8 0

596− put ((-1) :: Int) -- TMP HACK!

595+ UVar ns t -> do putWord8 0

596+ put ns

597+ put t

597598 UVal t -> do putWord8 1

598599 put t

599600

600601 get = do i <- getWord8

601602 case i of

602603 0 -> do x1 <- get

603− return (UVar x1)

604+ x2 <- get

605+ return (UVar x1 x2)

604606 1 -> do x1 <- get

605607 return (UVal x1)

606608 _ -> error "Corrupted binary data for UExp"

src/Idris/Core/Constraints.hs+19−20

@@ -16,17 +16,16 @@ import Data.List ( partition )

1616import qualified Data.Map.Strict as M

1717import qualified Data.Set as S

1818

19−

2019-- | Check that a list of universe constraints can be satisfied.

2120ucheck :: S.Set ConstraintFC -> TC ()

2221ucheck = void . solve 10 . S.filter (not . ignore)

2322 where

2423 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with

25− ignore (ConstraintFC c _) | any (== Var (-1)) (varsIn c) = True

24+ ignore (ConstraintFC c _) | any (== Var [] (-1)) (varsIn c) = True

2625 ignore (ConstraintFC (ULE a b) _) = a == b

2726 ignore _ = False

2827

29−newtype Var = Var Int

28+data Var = Var String Int

3029 deriving (Eq, Ord, Show)

3130

3231data Domain = Domain Int Int

@@ -72,12 +71,12 @@ solve maxUniverseLevel ucs =

7271 , cons_rhs = constraintsRHS

7372 }

7473

75− lhs (ULT (UVar x) _) = Just (Var x)

76− lhs (ULE (UVar x) _) = Just (Var x)

74+ lhs (ULT (UVar ns x) _) = Just (Var ns x)

75+ lhs (ULE (UVar ns x) _) = Just (Var ns x)

7776 lhs _ = Nothing

7877

79− rhs (ULT _ (UVar x)) = Just (Var x)

80− rhs (ULE _ (UVar x)) = Just (Var x)

78+ rhs (ULT _ (UVar ns x)) = Just (Var ns x)

79+ rhs (ULE _ (UVar ns x)) = Just (Var ns x)

8180 rhs _ = Nothing

8281

8382 -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)

@@ -148,38 +147,38 @@ solve maxUniverseLevel ucs =

148147 -- | look up the domain of a variable from the state.

149148 -- for convenience, this function also accepts UVal's and returns a singleton domain for them.

150149 domainOf :: MonadState SolverState m => UExp -> m Domain

151− domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)

150+ domainOf (UVar ns var) = gets (fst . (M.! Var ns var) . domainStore)

152151 domainOf (UVal val) = return (Domain val val)

153152

154153 asPair :: Domain -> (Int, Int)

155154 asPair (Domain x y) = (x, y)

156155

157156 updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()

158− updateUpperBoundOf suspect (UVar var) upper = do

157+ updateUpperBoundOf suspect (UVar ns var) upper = do

159158 doms <- gets domainStore

160− let (oldDom@(Domain lower _), suspects) = doms M.! Var var

159+ let (oldDom@(Domain lower _), suspects) = doms M.! Var ns var

161160 let newDom = Domain lower upper

162161 when (wipeOut newDom) $

163162 lift $ Error $

164− UniverseError (ufc suspect) (UVar var)

163+ UniverseError (ufc suspect) (UVar ns var)

165164 (asPair oldDom) (asPair newDom)

166165 (suspect : S.toList suspects)

167− modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }

168− addToQueueRHS (uconstraint suspect) (Var var)

166+ modify $ \ st -> st { domainStore = M.insert (Var ns var) (newDom, S.insert suspect suspects) doms }

167+ addToQueueRHS (uconstraint suspect) (Var ns var)

169168 updateUpperBoundOf _ UVal{} _ = return ()

170169

171170 updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()

172− updateLowerBoundOf suspect (UVar var) lower = do

171+ updateLowerBoundOf suspect (UVar ns var) lower = do

173172 doms <- gets domainStore

174− let (oldDom@(Domain _ upper), suspects) = doms M.! Var var

173+ let (oldDom@(Domain _ upper), suspects) = doms M.! Var ns var

175174 let newDom = Domain lower upper

176175 when (wipeOut newDom) $

177176 lift $ Error $

178− UniverseError (ufc suspect) (UVar var)

177+ UniverseError (ufc suspect) (UVar ns var)

179178 (asPair oldDom) (asPair newDom)

180179 (suspect : S.toList suspects)

181− modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }

182− addToQueueLHS (uconstraint suspect) (Var var)

180+ modify $ \ st -> st { domainStore = M.insert (Var ns var) (newDom, S.insert suspect suspects) doms }

181+ addToQueueLHS (uconstraint suspect) (Var ns var)

183182 updateLowerBoundOf _ UVal{} _ = return ()

184183

185184 -- | add all constraints (with the given var on the lhs) to the queue

@@ -224,5 +223,5 @@ ordNub = S.toList . S.fromList

224223

225224-- | variables in a constraint

226225varsIn :: UConstraint -> [Var]

227−varsIn (ULT a b) = [ Var v | UVar v <- [a,b] ]

228−varsIn (ULE a b) = [ Var v | UVar v <- [a,b] ]

226+varsIn (ULT a b) = [ Var ns v | UVar ns v <- [a,b] ]

227+varsIn (ULE a b) = [ Var ns v | UVar ns v <- [a,b] ]

src/Idris/Core/DeepSeq.hs+1−1

@@ -188,7 +188,7 @@ instance (NFData b) => NFData (Binder b) where

188188 rnf (PVTy x1) = rnf x1 `seq` ()

189189

190190instance NFData UExp where

191− rnf (UVar x1) = rnf x1 `seq` ()

191+ rnf (UVar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

192192 rnf (UVal x1) = rnf x1 `seq` ()

193193

194194instance NFData NameType where

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

@@ -151,6 +151,7 @@ execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)

151151execElab a e ps = execStateT e (ES (ps, a) "" Nothing)

152152

153153initElaborator :: Name -- ^ the name of what's to be elaborated

154+ -> String -- ^ the current source file

154155 -> Context -- ^ the current global context

155156 -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState

156157 -> Int -- ^ the value of the idris_name field of IState

@@ -158,9 +159,9 @@ initElaborator :: Name -- ^ the name of what's to be elaborated

158159 -> ProofState

159160initElaborator = newProof

160161

161−elaborate :: Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)

162−elaborate ctxt datatypes globalNames n ty d elab =

163− do let ps = initElaborator n ctxt datatypes globalNames ty

162+elaborate :: String -> Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)

163+elaborate tcns ctxt datatypes globalNames n ty d elab =

164+ do let ps = initElaborator n tcns ctxt datatypes globalNames ty

164165 (a, ES ps' str _) <- runElab d elab ps

165166 return $! (a, str)

166167

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

@@ -633,9 +633,11 @@ convEq ctxt holes topx topy = ceq [] topx topy where

633633 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

634634 ceq ps (App _ fx ax) (App _ fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)

635635 ceq ps (Constant x) (Constant y) = return (x == y)

636− ceq ps (TType x) (TType y) = do (v, cs) <- get

637− put (v, ULE x y : cs)

638− return True

636+ ceq ps (TType x) (TType y) | x == y = return True

637+ ceq ps (TType (UVal 0)) (TType y) = return True

638+ ceq ps (TType x) (TType y) = do (v, cs) <- get

639+ put (v, ULE x y : cs)

640+ return True

639641 ceq ps (UType AllTypes) x = return (isUsableUniverse x)

640642 ceq ps x (UType AllTypes) = return (isUsableUniverse x)

641643 ceq ps (UType u) (UType v) = return (u == v)

src/Idris/Core/ProofState.hs+10−8

@@ -60,7 +60,8 @@ data ProofState = PS { thname :: Name,

6060 unifylog :: Bool,

6161 done :: Bool,

6262 recents :: [Name],

63− while_elaborating :: [FailContext]

63+ while_elaborating :: [FailContext],

64+ constraint_ns :: String

6465 }

6566

6667data Tactic = Attack

@@ -319,19 +320,20 @@ addLog :: Monad m => String -> StateT TState m ()

319320addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

320321

321322newProof :: Name -- ^ the name of what's to be elaborated

323+ -> String -- ^ current source file

322324 -> Context -- ^ the current global context

323325 -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState

324326 -> Int -- ^ the value of the idris_name field of IState

325327 -> Type -- ^ the goal type

326328 -> ProofState

327−newProof n ctxt datatypes globalNames ty =

329+newProof n tcns ctxt datatypes globalNames ty =

328330 let h = holeName 0

329331 ty' = vToP ty

330332 in PS n [h] [] 1 globalNames (mkProofTerm (Bind h (Hole ty')

331333 (P Bound h ty'))) ty [] (h, []) [] []

332334 Nothing [] []

333335 [] [] [] []

334− Nothing ctxt datatypes "" False False [] []

336+ Nothing ctxt datatypes "" False False [] [] tcns

335337

336338type TState = ProofState -- [TacticAction])

337339type RunTactic = RunTactic' TState

@@ -468,7 +470,7 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

468470 (mkApp (P Ref n ty) (map getP (reverse env'))))

469471 where

470472 mkTy [] t = t

471− mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)

473+ mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar [] 0))) (mkTy bs t)

472474

473475 getP (n, b) = P Bound n (binderTy b)

474476defer dropped n ctxt env _ = fail "Can't defer a non-hole focus."

@@ -683,9 +685,9 @@ intro n ctxt env _ = fail "Can't introduce here."

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

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

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

686− unify' ctxt env (tyt, Nothing) (TType (UVar 0), Nothing)

687− unify' ctxt env (t, Nothing) (TType (UVar 0), Nothing)

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

688+ unify' ctxt env (tyt, Nothing) (TType (UVar [] 0), Nothing)

689+ unify' ctxt env (t, Nothing) (TType (UVar [] 0), Nothing)

690+ return $ Bind n (Pi impl tyv (TType (UVar [] 0))) (Bind x (Hole t) (P Bound x t))

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

690692

691693patvar :: Name -> RunTactic

@@ -1020,7 +1022,7 @@ matchProblems all ps updates probs = up updates probs where

10201022processTactic :: Tactic -> ProofState -> TC (ProofState, String)

10211023processTactic QED ps = case holes ps of

10221024 [] -> do let tm = {- normalise (context ps) [] -} getProofTerm (pterm ps)

1023− (tm', ty', _) <- recheck (context ps) [] (forget tm) tm

1025+ (tm', ty', _) <- recheck (constraint_ns ps) (context ps) [] (forget tm) tm

10241026 return (ps { done = True, pterm = mkProofTerm tm' },

10251027 "Proof complete: " ++ showEnv [] tm')

10261028 _ -> fail "Still holes to fill."

src/Idris/Core/TT.hs+8−4

@@ -38,7 +38,7 @@ module Idris.Core.TT(

3838 , bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact

3939 , discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname

4040 , fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv

41− , freeNames, getArgTys, getRetTy, implicitable, instantiate

41+ , freeNames, getArgTys, getRetTy, implicitable, instantiate, internalNS

4242 , intTyName, isInjective, isTypeConst, lookupCtxt

4343 , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth

4444 , nextName, noOccurrence, nsroot, occurrences

@@ -945,8 +945,11 @@ raw_unapply t = ua [] t where

945945

946946-- WELL TYPED TERMS ---------------------------------------------------------

947947

948+internalNS :: String

949+internalNS = "(internal)"

950+

948951-- | Universe expressions for universe checking

949−data UExp = UVar Int -- ^ universe variable

952+data UExp = UVar String Int -- ^ universe variable, with source file to disambiguate

950953 | UVal Int -- ^ explicit universe level

951954 deriving (Eq, Ord, Data, Typeable)

952955{-!

@@ -957,8 +960,9 @@ instance Sized UExp where

957960 size _ = 1

958961

959962instance Show UExp where

960− show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]

961− | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)

963+ show (UVar ns x)

964+ | x < 26 = ns ++ "." ++ [toEnum (x + fromEnum 'a')]

965+ | otherwise = ns ++ "." ++ toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)

962966 show (UVal x) = show x

963967-- show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")"

964968

src/Idris/Core/Typecheck.hs+27−28

@@ -58,22 +58,22 @@ isType ctxt env tm = isType' (normalise ctxt env tm)

5858 where isType' tm | isUniverse tm = return ()

5959 | otherwise = fail (showEnv env tm ++ " is not a Type")

6060

61−convType :: Context -> Env -> Term -> StateT UCs TC ()

62−convType ctxt env tm =

61+convType :: String -> Context -> Env -> Term -> StateT UCs TC ()

62+convType tcns ctxt env tm =

6363 do (v, cs) <- get

6464 put (v + 1, cs)

6565 case normalise ctxt env tm of

6666 UType _ -> return ()

67− _ -> convertsC ctxt env tm (TType (UVar v))

67+ _ -> convertsC ctxt env tm (TType (UVar tcns v))

6868

69−recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)

69+recheck :: String -> Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)

7070recheck = recheck_borrowing False []

7171

72−recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->

72+recheck_borrowing :: Bool -> [Name] -> String -> Context -> Env -> Raw -> Term ->

7373 TC (Term, Type, UCs)

74−recheck_borrowing uniq_check bs ctxt env tm orig

74+recheck_borrowing uniq_check bs tcns ctxt env tm orig

7575 = let v = next_tvar ctxt in

76− case runStateT (check' False ctxt env tm) (v, []) of -- holes banned

76+ case runStateT (check' False tcns ctxt env tm) (v, []) of -- holes banned

7777 Error (IncompleteTerm _) -> Error $ IncompleteTerm orig

7878 Error e -> Error e

7979 OK ((tm, ty), constraints) ->

@@ -82,10 +82,11 @@ recheck_borrowing uniq_check bs ctxt env tm orig

8282

8383check :: Context -> Env -> Raw -> TC (Term, Type)

8484check ctxt env tm

85− = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

85+ -- Holes allowed, so constraint namespace doesn't matter

86+ = evalStateT (check' True [] ctxt env tm) (0, [])

8687

87−check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

88−check' holes ctxt env top = chk (TType (UVar (-5))) env top where

88+check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

89+check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

8990

9091 smaller (UType NullType) _ = UType NullType

9192 smaller _ (UType NullType) = UType NullType

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

120121 case fty' of

121122 Bind x (Pi i (TType v') k) t ->

122123 do (v, cs) <- get

123− put (v+1, ULT (UVar v) v' : cs)

124+ put (v+1, ULT (UVar tcns v) v' : cs)

124125 let apty = simplify initContext env

125− (Bind x (Let (TType v') (TType (UVar v))) t)

126− return (App Complete fv (TType (UVar v)), apty)

126+ (Bind x (Let (TType v') (TType (UVar tcns v))) t)

127+ return (App Complete fv (TType (UVar tcns v)), apty)

127128 Bind x (Pi i s k) t ->

128129 do (av, aty) <- chk u env RType

129130 convertsC ctxt env aty s

@@ -150,9 +151,9 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

150151 chk u env RType

151152 | holes = return (TType (UVal 0), TType (UVal 0))

152153 | otherwise = do (v, cs) <- get

153− let c = ULT (UVar v) (UVar (v+1))

154+ let c = ULT (UVar tcns v) (UVar tcns (v+1))

154155 put (v+2, (c:cs))

155− return (TType (UVar v), TType (UVar (v+1)))

156+ return (TType (UVar tcns v), TType (UVar tcns (v+1)))

156157 chk u env (RUType un)

157158 | holes = return (UType un, TType (UVal 0))

158159 | otherwise = do -- TODO! Issue #1715 on the issue tracker.

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

181182 (v, cs) <- get

182183 (kv, kt) <- chk u env k -- no need to validate these constraints, they are independent

183184 put (v+1, cs)

184− let maxu = UVar v

185+ let maxu = UVar tcns v

185186 (tv, tt) <- chk st ((n, Pi i sv kv) : env) t

186187

187188-- convertsC ctxt env st (TType maxu)

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

195196 when (not holes) $ do (v, cs) <- get

196197 put (v, ULE su maxu :

197198 ULE tu maxu : cs)

198− let k' = TType (UVar v) `smaller` st `smaller` kv `smaller` u

199+ let k' = TType (UVar tcns v) `smaller` st `smaller` kv `smaller` u

199200 return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')

200201 (pToV n tv), k')

201202 (un, un') ->

@@ -225,33 +226,33 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

225226 where checkBinder (Lam t)

226227 = do (tv, tt) <- chk u env t

227228 let tv' = normalise ctxt env tv

228− convType ctxt env tt

229+ convType tcns ctxt env tt

229230 return (Lam tv, tt)

230231 checkBinder (Let t v)

231232 = do (tv, tt) <- chk u env t

232233 (vv, vt) <- chk u env v

233234 let tv' = normalise ctxt env tv

234235 convertsC ctxt env vt tv

235− convType ctxt env tt

236+ convType tcns ctxt env tt

236237 return (Let tv vv, tt)

237238 checkBinder (NLet t v)

238239 = do (tv, tt) <- chk u env t

239240 (vv, vt) <- chk u env v

240241 let tv' = normalise ctxt env tv

241242 convertsC ctxt env vt tv

242− convType ctxt env tt

243+ convType tcns ctxt env tt

243244 return (NLet tv vv, tt)

244245 checkBinder (Hole t)

245246 | not holes = lift $ tfail (IncompleteTerm undefined)

246247 | otherwise

247248 = do (tv, tt) <- chk u env t

248249 let tv' = normalise ctxt env tv

249− convType ctxt env tt

250+ convType tcns ctxt env tt

250251 return (Hole tv, tt)

251252 checkBinder (GHole i ns t)

252253 = do (tv, tt) <- chk u env t

253254 let tv' = normalise ctxt env tv

254− convType ctxt env tt

255+ convType tcns ctxt env tt

255256 return (GHole i ns tv, tt)

256257 checkBinder (Guess t v)

257258 | not holes = lift $ tfail (IncompleteTerm undefined)

@@ -260,19 +261,19 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

260261 (vv, vt) <- chk u env v

261262 let tv' = normalise ctxt env tv

262263 convertsC ctxt env vt tv

263− convType ctxt env tt

264+ convType tcns ctxt env tt

264265 return (Guess tv vv, tt)

265266 checkBinder (PVar t)

266267 = do (tv, tt) <- chk u env t

267268 let tv' = normalise ctxt env tv

268− convType ctxt env tt

269+ convType tcns ctxt env tt

269270 -- Normalised version, for erasure purposes (it's easier

270271 -- to tell if it's a collapsible variable)

271272 return (PVar tv, tt)

272273 checkBinder (PVTy t)

273274 = do (tv, tt) <- chk u env t

274275 let tv' = normalise ctxt env tv

275− convType ctxt env tt

276+ convType tcns ctxt env tt

276277 return (PVTy tv, tt)

277278

278279 discharge n (Lam t) bt scv sct

@@ -339,9 +340,7 @@ checkUnique borrowed ctxt env tm

339340 StateT [(Name, (UniqueUse, Universe))] TC ()

340341 chkBinderName env n b

341342 = do let rawty = forgetEnv (map fst env) (binderTy b)

342− (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?

343− -- Issue #1714 on the issue tracker

344− -- https://github.com/idris-lang/Idris-dev/issues/1714

343+ (_, kind) <- lift $ check ctxt env rawty

345344 case kind of

346345 UType UniqueType -> do ns <- get

347346 if n `elem` borrowed

src/Idris/Core/Unify.hs+2−2

@@ -494,14 +494,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

494494 un' env fn bnames (App _ f x) (Bind n (Pi i t k) y)

495495 | noOccurrence n y && injectiveApp f

496496 = do ux <- un' env False bnames x y

497− uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

497+ uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar [] 0)))

498498 (Bind n (Pi i t k) (V 1)))

499499 combine env bnames ux uf

500500

501501 un' env fn bnames (Bind n (Pi i t k) y) (App _ f x)

502502 | noOccurrence n y && injectiveApp f

503503 = do ux <- un' env False bnames y x

504− uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

504+ uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar [] 0)))

505505 (Bind n (Pi i t k) (V 1))) f

506506 combine env bnames ux uf

507507

src/Idris/DeepSeq.hs+1

@@ -318,6 +318,7 @@ instance NFData IBCWrite where

318318 rnf (IBCDeprecate n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

319319 rnf (IBCRecord x) = rnf x `seq` ()

320320 rnf (IBCFragile n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

321+ rnf (IBCConstraint n1 n2) = rnf n1 `seq` rnf n2 `seq` ()

321322

322323

323324instance NFData a => NFData (D.Block a) where

src/Idris/Elab/Clause.hs+18−17

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

497497 i <- getIState

498498 let lhs = addImplPat i lhs_in

499499 -- if the LHS type checks, it is possible

500− case elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

500+ case elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

501501 (erun fc (buildTC i info ELHS [] fname

502502 (allNamesIn lhs_in)

503503 (infTerm lhs))) of

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

507507 sendHighlighting highlights

508508 updateIState $ \i -> i { idris_name = newGName }

509509 let lhs_tm = orderPats (getInferTerm lhs')

510− case recheck ctxt' [] (forget lhs_tm) lhs_tm of

510+ case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of

511511 OK _ -> return True

512512 err -> return False

513513 -- if it's a recoverable error, the case may become possible

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

580580 "\n" ++ show (fn_ty, fn_is))

581581

582582 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-

583− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

583+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

584584 (do res <- errAt "left hand side of " fname Nothing

585585 (erun fc (buildTC i info ELHS opts fname

586586 (allNamesIn lhs_in)

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

608608 ctxt <- getContext

609609 (clhs_c, clhsty) <- if not inf

610610 then recheckC_borrowing False (PEGenerated `notElem` opts)

611− [] fc id [] lhs_tm

611+ [] (constraintNS info) fc id [] lhs_tm

612612 else return (lhs_tm, lhs_ty)

613613 let clhs = Idris.Core.Evaluate.simplify ctxt [] clhs_c

614614 let borrowed = borrowedNames [] clhs

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

666666 ctxt <- getContext -- new context with where block added

667667 logElab 5 "STARTING CHECK"

668668 ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-

669− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState

669+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState

670670 (do pbinds ist lhs_tm

671671 -- proof search can use explicitly written names

672672 mapM_ addPSname (allNamesIn lhs_in)

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

697697 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)

698698

699699 -- If there's holes, set the metavariables as undefinable

700− def' <- checkDef fc (\n -> Elaborating "deferred type of " n Nothing) (null holes) defer

700+ def' <- checkDef info fc (\n -> Elaborating "deferred type of " n Nothing) (null holes) defer

701701 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, null holes))) def'

702702 addDeferred def''

703703

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

723723 -- things)

724724 <- if (null holes || null def') && not inf

725725 then recheckC_borrowing True (PEGenerated `notElem` opts)

726− borrowed fc id [] rhs'

726+ borrowed (constraintNS info) fc id [] rhs'

727727 else return (rhs', clhsty)

728728

729729 logElab 6 $ " ==> " ++ showEnvDbg [] crhsty ++ " against " ++ showEnvDbg [] clhsty

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

738738 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

739739 OK (_, cs) -> when (PEGenerated `notElem` opts) $ do

740740 addConstraints fc cs

741+ mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

741742 logElab 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)

742743 return ()

743744 Error e -> ierror (At fc (CantUnify False (clhsty, Nothing) (crhsty, Nothing) e [] 0))

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

832833 (addImplPat i lhs_in)

833834 logElab 2 ("LHS: " ++ show lhs)

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

835− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

836+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

836837 (errAt "left hand side of with in " fname Nothing

837838 (erun fc (buildTC i info ELHS opts fname

838839 (allNamesIn lhs_in)

@@ -848,14 +849,14 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

848849 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

849850 let static_names = getStaticNames i lhs_tm

850851 logElab 5 (show lhs_tm ++ "\n" ++ show static_names)

851− (clhs, clhsty) <- recheckC fc id [] lhs_tm

852+ (clhs, clhsty) <- recheckC (constraintNS info) fc id [] lhs_tm

852853 logElab 5 ("Checked " ++ show clhs)

853854 let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))

854855 let wval = rhs_trans info $ addImplBound i (map fst bargs) wval_in

855856 logElab 5 ("Checking " ++ showTmImpls wval)

856857 -- Elaborate wval in this context

857858 ((wval', defer, is, ctxt', newDecls, highlights, newGName), _) <-

858− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")

859+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")

859860 (bindTyArgs PVTy bargs infP) initEState

860861 (do pbinds i lhs_tm

861862 -- proof search can use explicitly written names

@@ -872,14 +873,14 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

872873 sendHighlighting highlights

873874 updateIState $ \i -> i { idris_name = newGName }

874875

875− def' <- checkDef fc iderr True defer

876+ def' <- checkDef info fc iderr True defer

876877 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

877878 addDeferred def''

878879 mapM_ (elabCaseBlock info opts) is

879880 logElab 5 ("Checked wval " ++ show wval')

880881

881882 ctxt <- getContext

882− (cwval, cwvalty) <- recheckC fc id [] (getInferTerm wval')

883+ (cwval, cwvalty) <- recheckC (constraintNS info) fc id [] (getInferTerm wval')

883884 let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)

884885 let cwvalN = explicitNames (normalise ctxt [] cwval)

885886 logElab 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

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

914915 let wargname = sMN windex "warg"

915916

916917 logElab 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

917− let wtype = bindTyArgs (flip (Pi Nothing) (TType (UVar 0))) (bargs_pre ++

918+ let wtype = bindTyArgs (flip (Pi Nothing) (TType (UVar [] 0))) (bargs_pre ++

918919 (wargname, wargtype) :

919920 map (abstract wargname wargval wargtype) bargs_post ++

920921 case mpn of

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

937938 addIBC (IBCImp wname)

938939 addIBC (IBCStatic wname)

939940

940− def' <- checkDef fc iderr True [(wname, (-1, Nothing, wtype, []))]

941+ def' <- checkDef info fc iderr True [(wname, (-1, Nothing, wtype, []))]

941942 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

942943 addDeferred def''

943944

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

970971 ctxt <- getContext -- New context with block added

971972 i <- getIState

972973 ((rhs', defer, is, ctxt', newDecls, highlights, newGName), _) <-

973− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState

974+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState

974975 (do pbinds i lhs_tm

975976 setNextName

976977 (ElabResult _ d is ctxt' newDecls highlights newGName) <-

@@ -983,12 +984,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

983984 sendHighlighting highlights

984985 updateIState $ \i -> i { idris_name = newGName }

985986

986− def' <- checkDef fc iderr True defer

987+ def' <- checkDef info fc iderr True defer

987988 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

988989 addDeferred def''

989990 mapM_ (elabCaseBlock info opts) is

990991 logElab 5 ("Checked RHS " ++ show rhs')

991− (crhs, crhsty) <- recheckC fc id [] rhs'

992+ (crhs, crhsty) <- recheckC (constraintNS info) fc id [] rhs'

992993 return $ (Right (clhs, crhs), lhs)

993994 where

994995 getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t

src/Idris/Elab/Data.hs+7−6

@@ -287,6 +287,7 @@ addParamConstraints fc ps cty cons

287287 then ULE avar cvar

288288 else ULT avar cvar

289289 addConstraints fc (tv, [con])

290+ addIBC (IBCConstraint fc con)

290291 _ -> return ()

291292 constraintTy t = return ()

292293

@@ -318,30 +319,30 @@ elabCaseFun ind paramPos n ty cons info = do

318319 let motiveConstr = [(motiveName, expl, motive)]

319320 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

320321 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC [] n) scrutineeIdxs) (PRef elimFC [] scrutineeName))

321− let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName NoFC eliminatorTy

322+ let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName elimFC eliminatorTy

322323 let clauseConsElimArgs = map getPiName consTerms

323324 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

324325 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC [] arg)) clauseGeneralArgs'

325326 let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy

326327 elimLog elimSig

327328 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

328− let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

329+ let eliminatorDef = PClauses elimFC [TotalFn] elimDeclName eliminatorClauses

329330 elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

330331 State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)

331332 (ierror . Elaborating "type declaration of " elimDeclName Nothing)

332333 -- Do not elaborate clauses if there aren't any

333334 case eliminatorClauses of

334− [] -> State.lift $ solveDeferred emptyFC elimDeclName -- Remove meta-variable for type

335+ [] -> State.lift $ solveDeferred elimFC elimDeclName -- Remove meta-variable for type

335336 _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)

336337 (ierror . Elaborating "clauses of " elimDeclName Nothing)

337338 where elimLog :: String -> EliminatorState ()

338339 elimLog s = State.lift (logElab 2 s)

339340

340341 elimFC :: FC

341− elimFC = fileFC "(casefun)"

342+ elimFC = fileFC $ "(casefun " ++ show n ++ ")"

342343

343344 elimDeclName :: Name

344− elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' emptyFC) $ n

345+ elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n

345346

346347 applyNS :: Name -> [String] -> Name

347348 applyNS n [] = n

@@ -415,7 +416,7 @@ elabCaseFun ind paramPos n ty cons info = do

415416

416417 piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm

417418 piConstr [] ty = ty

418− piConstr ((n, pl, tyb):tyr) ty = PPi pl n NoFC tyb (piConstr tyr ty)

419+ piConstr ((n, pl, tyb):tyr) ty = PPi pl n elimFC tyb (piConstr tyr ty)

419420

420421 interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]

421422 interlievePos idxs [] l2 i = l2

src/Idris/Elab/Instance.hs+4−4

@@ -217,8 +217,8 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

217217 mkiname n' ns ps' expn' =

218218 case expn' of

219219 Nothing -> case ns of

220− Nothing -> SN (sInstanceN n' (map show ps'))

221− Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

220+ [] -> SN (sInstanceN n' (map show ps'))

221+ m -> sNS (SN (sInstanceN n' (map show ps'))) m

222222 Just nm -> nm

223223

224224 substInstance ips pnames (PInstance doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)

@@ -245,7 +245,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

245245 let ty = addImpl [] i ty'

246246 ctxt <- getContext

247247 (ElabResult tyT _ _ ctxt' newDecls highlights newGName, _) <-

248− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) iname (TType (UVal 0)) initEState

248+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) iname (TType (UVal 0)) initEState

249249 (errAt "type of " iname Nothing (erun fc (build i info ERHS [] iname ty)))

250250 setContext ctxt'

251251 processTacticDecls info newDecls

@@ -253,7 +253,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

253253 updateIState $ \i -> i { idris_name = newGName }

254254

255255 ctxt <- getContext

256− (cty, _) <- recheckC fc id [] tyT

256+ (cty, _) <- recheckC (constraintNS info) fc id [] tyT

257257 let nty = normalise ctxt [] cty

258258 return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (map fst $ class_instances ci)

259259

src/Idris/Elab/RunElab.hs+2−2

@@ -40,9 +40,9 @@ elabRunElab info fc script' ns =

4040 ist <- getIState

4141 ctxt <- getContext

4242 (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-

43− tclift $ elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState

43+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState

4444 (transformErr RunningElabScript

45− (erun fc (do tm <- runElabAction ist fc [] script ns

45+ (erun fc (do tm <- runElabAction info ist fc [] script ns

4646 EState is _ impls highlights _ _ <- getAux

4747 ctxt <- get_context

4848 let ds = [] -- todo

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

@@ -815,8 +815,8 @@ elab ist info emode opts fn tm

815815 mkN n@(NS _ _) = n

816816 mkN n@(SN _) = n

817817 mkN n = case namespace info of

818− Just xs@(_:_) -> sNS n xs

819− _ -> n

818+ xs@(_:_) -> sNS n xs

819+ _ -> n

820820

821821 elab' ina _ (PMatchApp fc fn)

822822 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

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

10891089-- mkCaseName (MN i x) = MN i (x ++ "_case")

10901090 mkN n@(NS _ _) = n

10911091 mkN n = case namespace info of

1092− Just xs@(_:_) -> sNS n xs

1092+ xs@(_:_) -> sNS n xs

10931093 _ -> n

10941094

10951095 getScrType [] = Nothing

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

11571157 g_nextname <- get_global_nextname

11581158 saveState

11591159 updatePS (const .

1160− newProof (sMN 0 "q") ctxt datatypes g_nextname $

1160+ newProof (sMN 0 "q") (constraintNS info) ctxt datatypes g_nextname $

11611161 P Ref (reflm "TT") Erased)

11621162

11631163 -- Re-add the unquotes, letting Idris infer the (fictional)

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

12081208 _ -> False

12091209 case quoted of

12101210 Just q -> do ctxt <- get_context

1211− (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1211+ (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

12121212 if pattern

12131213 then if isRaw

12141214 then reflectRawQuotePattern unquoteNames (forget q')

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

12791279 fullyElaborated script

12801280 solve -- eliminate the hole. Becuase there are no references, the script is only in the binding

12811281 env <- get_env

1282− runElabAction ist (maybe fc' id fc) env script ns

1282+ runElabAction info ist (maybe fc' id fc) env script ns

12831283 solve

12841284 elab' ina fc (PConstSugar constFC tm) =

12851285 -- Here we elaborate the contained term, then calculate

@@ -1862,14 +1862,14 @@ case_ ind autoSolve ist fn tm = do

18621862 when autoSolve solveAll

18631863

18641864-- | Compute the appropriate name for a top-level metavariable

1865−metavarName :: Maybe [String] -> Name -> Name

1866−metavarName _ n@(NS _ _) = n

1867−metavarName (Just (ns@(_:_))) n = sNS n ns

1868−metavarName _ n = n

1865+metavarName :: [String] -> Name -> Name

1866+metavarName _ n@(NS _ _) = n

1867+metavarName (ns@(_:_)) n = sNS n ns

1868+metavarName _ n = n

18691869

1870−runElabAction :: IState -> FC -> Env -> Term -> [String] -> ElabD Term

1871−runElabAction ist fc env tm ns = do tm' <- eval tm

1872− runTacTm tm'

1870+runElabAction :: ElabInfo -> IState -> FC -> Env -> Term -> [String] -> ElabD Term

1871+runElabAction info ist fc env tm ns = do tm' <- eval tm

1872+ runTacTm tm'

18731873

18741874 where

18751875 eval tm = do ctxt <- get_context

@@ -1899,7 +1899,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

18991899 _ -> P Ref n Erased

19001900 fakeTT (RBind n b body) = Bind n (fmap fakeTT b) (fakeTT body)

19011901 fakeTT (RApp f a) = App Complete (fakeTT f) (fakeTT a)

1902− fakeTT RType = TType (UVar (-1))

1902+ fakeTT RType = TType (UVar [] (-1))

19031903 fakeTT (RUType u) = UType u

19041904 fakeTT (RConstant c) = Constant c

19051905

@@ -2308,10 +2308,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

23082308 (ctxt', ES (p, aux') _ _) <-

23092309 do (ES (current_p, _) _ _) <- get

23102310 lift $ runElab aux

2311− (do runElabAction ist fc [] script ns

2311+ (do runElabAction info ist fc [] script ns

23122312 ctxt' <- get_context

23132313 return ctxt')

2314− ((newProof recH ctxt datatypes g_next goalTT)

2314+ ((newProof recH (constraintNS info) ctxt datatypes g_next goalTT)

23152315 { nextname = nextname current_p })

23162316 set_context ctxt'

23172317

@@ -2322,7 +2322,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

23222322 }

23232323 put (ES (p', aux') s e)

23242324 env' <- get_env

2325− (tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out

2325+ (tm, ty, _) <- lift $ recheck (constraintNS info) ctxt' env (forget tm_out) tm_out

23262326 let (tm', ty') = (reflect tm, reflect ty)

23272327 fmap fst . checkClosed $

23282328 rawPair (Var $ reflm "TT", Var $ reflm "TT")

@@ -2333,7 +2333,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

23332333 ptm <- get_term

23342334 -- See documentation above in the elab case for PMetavar

23352335 let unique_used = getUniqueUsed ctxt ptm

2336− let mvn = metavarName (Just ns) n'

2336+ let mvn = metavarName ns n'

23372337 attack

23382338 defer unique_used mvn

23392339 solve

@@ -2699,7 +2699,7 @@ processTacticDecls info steps =

26992699 updateIState $ \i -> i { idris_implicits =

27002700 addDef n impls (idris_implicits i) }

27012701 addIBC (IBCImp n)

2702− ds <- checkDef fc (\_ e -> e) True [(n, (-1, Nothing, ty, []))]

2702+ ds <- checkDef info fc (\_ e -> e) True [(n, (-1, Nothing, ty, []))]

27032703 addIBC (IBCDef n)

27042704 ctxt <- getContext

27052705 case lookupDef n ctxt of

@@ -2817,7 +2817,7 @@ processTacticDecls info steps =

28172817 let lhs = addImplPat ist lhs_in

28182818 let fc = fileFC "elab_reflected_totality"

28192819 let tcgen = False -- TODO: later we may support dictionary generation

2820− case elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState

2820+ case elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState

28212821 (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)

28222822 (infTerm lhs))) of

28232823 OK (ElabResult lhs' _ _ _ _ _ name', _) ->

@@ -2825,7 +2825,7 @@ processTacticDecls info steps =

28252825 -- want to run infinitely many times

28262826 let lhs_tm = orderPats (getInferTerm lhs')

28272827 updateIState $ \i -> i { idris_name = name' }

2828− case recheck ctxt [] (forget lhs_tm) lhs_tm of

2828+ case recheck (constraintNS info) ctxt [] (forget lhs_tm) lhs_tm of

28292829 OK _ -> return True

28302830 err -> return False

28312831 -- if it's a recoverable error, the case may become possible

src/Idris/Elab/Transform.hs+4−4

@@ -62,7 +62,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

6262 let lhs = addImplPat i lhs_in

6363 logElab 5 ("Transform LHS input: " ++ showTmImpls lhs)

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

65− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transLHS") infP initEState

65+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transLHS") infP initEState

6666 (erun fc (buildTC i info ETransLHS [] (sUN "transform")

6767 (allNamesIn lhs_in) (infTerm lhs)))

6868 setContext ctxt'

@@ -73,7 +73,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

7373 let lhs_ty = getInferType lhs'

7474 let newargs = pvars i lhs_tm

7575

76− (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] fc id [] lhs_tm

76+ (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] lhs_tm

7777 let clhs_tm = renamepats pnames clhs_tm_in

7878 logElab 3 ("Transform LHS " ++ show clhs_tm)

7979 logElab 3 ("Transform type " ++ show clhs_ty)

@@ -82,7 +82,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

8282 logElab 5 ("Transform RHS input: " ++ showTmImpls rhs)

8383

8484 ((rhs', defer, ctxt', newDecls, newGName), _) <-

85− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transRHS") clhs_ty initEState

85+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transRHS") clhs_ty initEState

8686 (do pbinds i lhs_tm

8787 setNextName

8888 (ElabResult _ _ _ ctxt' newDecls highlights newGName) <- erun fc (build i info ERHS [] (sUN "transform") rhs)

@@ -97,7 +97,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

9797 sendHighlighting highlights

9898 updateIState $ \i -> i { idris_name = newGName }

9999

100− (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] fc id [] rhs'

100+ (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] rhs'

101101 let crhs_tm = renamepats pnames crhs_tm_in

102102 logElab 3 ("Transform RHS " ++ show crhs_tm)

103103

src/Idris/Elab/Type.hs+5−5

@@ -82,7 +82,7 @@ buildType info syn fc opts n ty' = do

8282 logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

8383

8484 ((ElabResult tyT' defer is ctxt' newDecls highlights newGName, est), log) <-

85− tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState

85+ tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState

8686 (errAt "type of " n Nothing

8787 (erunAux fc (build i info ETyDecl [] n ty)))

8888

@@ -96,7 +96,7 @@ buildType info syn fc opts n ty' = do

9696

9797 logElab 3 $ show ty ++ "\nElaborated: " ++ show tyT'

9898

99− ds <- checkAddDef True False fc iderr True defer

99+ ds <- checkAddDef True False info fc iderr True defer

100100 -- if the type is not complete, note that we'll need to infer

101101 -- things later (for solving metavariables)

102102 when (length ds > length is) -- more deferred than case blocks

@@ -107,7 +107,7 @@ buildType info syn fc opts n ty' = do

107107 logElab 5 $ "Rechecking"

108108 logElab 6 $ show tyT

109109 logElab 10 $ "Elaborated to " ++ showEnvDbg [] tyT

110− (cty, ckind) <- recheckC fc id [] tyT

110+ (cty, ckind) <- recheckC (constraintNS info) fc id [] tyT

111111

112112 -- record the implicit and inaccessible arguments

113113 i <- getIState

@@ -140,7 +140,7 @@ buildType info syn fc opts n ty' = do

140140

141141 return (cty, ckind, ty, inacc)

142142 where

143− patToImp (Bind n (PVar t) sc) = Bind n (Pi Nothing t (TType (UVar 0))) (patToImp sc)

143+ patToImp (Bind n (PVar t) sc) = Bind n (Pi Nothing t (TType (UVar [] 0))) (patToImp sc)

144144 patToImp (Bind n b sc) = Bind n b (patToImp sc)

145145 patToImp t = t

146146

@@ -203,7 +203,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

203203 -- Productivity checking now via checking for guarded 'Delay'

204204 let opts' = opts -- if corec then (Coinductive : opts) else opts

205205 let usety = if norm then nty' else nty

206− ds <- checkDef fc iderr True [(n, (-1, Nothing, usety, []))]

206+ ds <- checkDef info fc iderr True [(n, (-1, Nothing, usety, []))]

207207 addIBC (IBCDef n)

208208 addDefinedName n

209209 let ds' = map (\(n, (i, top, fam, ns)) -> (n, (i, top, fam, ns, True, True))) ds

src/Idris/Elab/Utils.hs+13−11

@@ -35,17 +35,19 @@ import qualified Data.Map as Map

3535

3636recheckC = recheckC_borrowing False True []

3737

38−recheckC_borrowing uniq_check addConstrs bs fc mkerr env t

38+recheckC_borrowing uniq_check addConstrs bs tcns fc mkerr env t

3939 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

40+

4041 ctxt <- getContext

4142 t' <- case safeForget t of

4243 Just ft -> return ft

4344 Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))

44− (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of

45+ (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs tcns ctxt env t' t of

4546 Error e -> tfail (At fc (mkerr e))

4647 OK x -> return x

4748 logElab 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

48− when addConstrs $ addConstraints fc cs

49+ when addConstrs $ do addConstraints fc cs

50+ mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

4951 mapM_ (checkDeprecated fc) (allTTNames tm)

5052 mapM_ (checkDeprecated fc) (allTTNames ty)

5153 mapM_ (checkFragile fc) (allTTNames tm)

@@ -80,23 +82,23 @@ checkFragile fc n = do

8082iderr :: Name -> Err -> Err

8183iderr _ e = e

8284

83−checkDef :: FC -> (Name -> Err -> Err) -> Bool ->

85+checkDef :: ElabInfo -> FC -> (Name -> Err -> Err) -> Bool ->

8486 [(Name, (Int, Maybe Name, Type, [Name]))] ->

8587 Idris [(Name, (Int, Maybe Name, Type, [Name]))]

86−checkDef fc mkerr definable ns

87− = checkAddDef False True fc mkerr definable ns

88+checkDef info fc mkerr definable ns

89+ = checkAddDef False True info fc mkerr definable ns

8890

89−checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err) -> Bool

91+checkAddDef :: Bool -> Bool -> ElabInfo -> FC -> (Name -> Err -> Err) -> Bool

9092 -> [(Name, (Int, Maybe Name, Type, [Name]))]

9193 -> Idris [(Name, (Int, Maybe Name, Type, [Name]))]

92−checkAddDef add toplvl fc mkerr def [] = return []

93−checkAddDef add toplvl fc mkerr definable ((n, (i, top, t, psns)) : ns)

94+checkAddDef add toplvl info fc mkerr def [] = return []

95+checkAddDef add toplvl info fc mkerr definable ((n, (i, top, t, psns)) : ns)

9496 = do ctxt <- getContext

9597 logElab 5 $ "Rechecking deferred name " ++ show (n, t, definable)

96− (t', _) <- recheckC fc (mkerr n) [] t

98+ (t', _) <- recheckC (constraintNS info) fc (mkerr n) [] t

9799 when add $ do addDeferred [(n, (i, top, t, psns, toplvl, definable))]

98100 addIBC (IBCDef n)

99− ns' <- checkAddDef add toplvl fc mkerr definable ns

101+ ns' <- checkAddDef add toplvl info fc mkerr definable ns

100102 return ((n, (i, top, t', psns)) : ns')

101103

102104-- | Get the list of (index, name) of inaccessible arguments from an elaborated

src/Idris/Elab/Value.hs+3−3

@@ -74,7 +74,7 @@ elabValBind info aspat norm tm_in

7474 -- * elaboration as a function a -> b

7575

7676 (ElabResult tm' defer is ctxt' newDecls highlights newGName, _) <-

77− tclift (elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "val") infP initEState

77+ tclift (elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "val") infP initEState

7878 (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

7979

8080 -- Extend the context with new definitions created

@@ -85,13 +85,13 @@ elabValBind info aspat norm tm_in

8585

8686 let vtm = orderPats (getInferTerm tm')

8787

88− def' <- checkDef (fileFC "(input)") iderr True defer

88+ def' <- checkDef info (fileFC "(input)") iderr True defer

8989 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) def'

9090 addDeferred def''

9191 mapM_ (elabCaseBlock info []) is

9292

9393 logElab 3 ("Value: " ++ show vtm)

94− (vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm

94+ (vtm_in, vty) <- recheckC (constraintNS info) (fileFC "(input)") id [] vtm

9595

9696 let vtm = if norm then normalise (tt_ctxt i) [] vtm_in

9797 else vtm_in

src/Idris/ElabDecls.hs+16−14

@@ -71,12 +71,12 @@ import Util.Pretty(pretty, text)

7171

7272

7373-- | Top level elaborator info, supporting recursive elaboration

74−recinfo :: ElabInfo

75−recinfo = EInfo [] emptyContext id Nothing Nothing 0 id elabDecl'

74+recinfo :: FC -> ElabInfo

75+recinfo fc = EInfo [] emptyContext id [] (Just fc) (fc_fname fc) 0 id elabDecl'

7676

7777-- | Return the elaborated term which calls 'main'

7878elabMain :: Idris Term

79−elabMain = do (m, _) <- elabVal recinfo ERHS

79+elabMain = do (m, _) <- elabVal (recinfo fc) ERHS

8080 (PApp fc (PRef fc [] (sUN "run__IO"))

8181 [pexp $ PRef fc [] (sNS (sUN "main") ["Main"])])

8282 return m

@@ -89,12 +89,12 @@ elabPrims = do i <- getIState

8989 let mkdec opt decl docs argdocs =

9090 PData docs argdocs defaultSyntax (fileFC "builtin")

9191 opt decl

92− elabDecl' EAll recinfo (mkdec inferOpts inferDecl emptyDocstring [])

92+ elabDecl' EAll (recinfo primfc) (mkdec inferOpts inferDecl emptyDocstring [])

9393 -- We don't want the constraints generated by 'Infer' since

9494 -- it's only scaffolding for the elaborator

9595 i <- getIState

9696 putIState $ i { idris_constraints = cs_in }

97− elabDecl' EAll recinfo (mkdec eqOpts eqDecl eqDoc eqParamDoc)

97+ elabDecl' EAll (recinfo primfc) (mkdec eqOpts eqDecl eqDoc eqParamDoc)

9898

9999 addNameHint eqTy (sUN "prf")

100100 mapM_ elabPrim primitives

@@ -109,6 +109,8 @@ elabPrims = do i <- getIState

109109 i <- getIState

110110 putIState i { idris_scprims = (n, sc) : idris_scprims i }

111111

112+ primfc = fileFC "primitive"

113+

112114 valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value

113115 valuePrim prim vals = fmap VConstant (mapM getConst vals >>= prim)

114116

@@ -118,9 +120,9 @@ elabPrims = do i <- getIState

118120

119121 p_believeMe [_,_,x] = Just x

120122 p_believeMe _ = Nothing

121− believeTy = Bind (sUN "a") (Pi Nothing (TType (UVar (-2))) (TType (UVar (-1))))

122− (Bind (sUN "b") (Pi Nothing (TType (UVar (-2))) (TType (UVar (-1))))

123− (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar (-1)))) (V 1)))

123+ believeTy = Bind (sUN "a") (Pi Nothing (TType (UVar [] (-2))) (TType (UVar [] (-1))))

124+ (Bind (sUN "b") (Pi Nothing (TType (UVar [] (-2))) (TType (UVar [] (-1))))

125+ (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar [] (-1)))) (V 1)))

124126 elabBelieveMe

125127 = do let prim__believe_me = sUN "prim__believe_me"

126128 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

@@ -143,10 +145,10 @@ elabPrims = do i <- getIState

143145 vnNothing = VP (DCon 0 1 False) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

144146 vnRefl = VP (DCon 0 2 False) eqCon VErased

145147

146− synEqTy = Bind (sUN "a") (Pi Nothing (TType (UVar (-3))) (TType (UVar (-2))))

147− (Bind (sUN "b") (Pi Nothing (TType (UVar (-3))) (TType (UVar (-2))))

148− (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar (-2))))

149− (Bind (sUN "y") (Pi Nothing (V 1) (TType (UVar (-2))))

148+ synEqTy = Bind (sUN "a") (Pi Nothing (TType (UVar [] (-3))) (TType (UVar [] (-2))))

149+ (Bind (sUN "b") (Pi Nothing (TType (UVar [] (-3))) (TType (UVar [] (-2))))

150+ (Bind (sUN "x") (Pi Nothing (V 1) (TType (UVar [] (-2))))

151+ (Bind (sUN "y") (Pi Nothing (V 1) (TType (UVar [] (-2))))

150152 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)

151153 [V 3, V 2, V 1, V 0]]))))

152154 elabSynEq

@@ -262,8 +264,8 @@ elabDecl' what info (PNamespace n nfc ps) =

262264 let ns = reverse (map T.pack newNS)

263265 sendHighlighting [(nfc, AnnNamespace ns Nothing)]

264266 where

265− newNS = maybe [n] (n:) (namespace info)

266− ninfo = info { namespace = Just newNS }

267+ newNS = n : namespace info

268+ ninfo = info { namespace = newNS }

267269

268270elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)

269271 | what /= EDefns

src/Idris/Error.hs+2−1

@@ -28,6 +28,7 @@ import System.IO.Error(isUserError, ioeGetErrorString)

2828import Data.Char

2929import Data.List (intercalate, isPrefixOf)

3030import qualified Data.Text as T

31+import qualified Data.Set as S

3132import Data.Typeable

3233import qualified Data.Traversable as Traversable

3334import qualified Data.Foldable as Foldable

@@ -36,7 +37,7 @@ iucheck :: Idris ()

3637iucheck = do tit <- typeInType

3738 ist <- getIState

3839 let cs = idris_constraints ist

39− logLvl 7 $ "ALL CONSTRAINTS: " ++ show cs

40+ logLvl 7 $ "ALL CONSTRAINTS: " ++ show (length (S.toList cs))

4041 when (not tit) $

4142 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`

4243 (\e -> do let fc = getErrSpan e

src/Idris/IBC.hs+14−2

@@ -46,8 +46,10 @@ import System.FilePath

4646import System.Directory

4747import Codec.Archive.Zip

4848

49+import Debug.Trace

50+

4951ibcVersion :: Word16

50−ibcVersion = 143

52+ibcVersion = 144

5153

5254-- | When IBC is being loaded - we'll load different things (and omit

5355-- different structures/definitions) depending on which phase we're in.

@@ -105,6 +107,7 @@ data IBCFile = IBCFile {

105107 , ibc_injective :: ![(Name, Injectivity)]

106108 , ibc_access :: ![(Name, Accessibility)]

107109 , ibc_fragile :: ![(Name, String)]

110+ , ibc_constraints :: ![(FC, UConstraint)]

108111 }

109112 deriving Show

110113{-!

@@ -112,7 +115,7 @@ deriving instance Binary IBCFile

112115!-}

113116

114117initIBC :: IBCFile

115−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] []

118+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

116119

117120hasValidIBCVersion :: FilePath -> Idris Bool

118121hasValidIBCVersion fp = do

@@ -208,6 +211,8 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

208211 makeEntry "ibc_injective" (ibc_injective i),

209212 makeEntry "ibc_access" (ibc_access i),

210213 makeEntry "ibc_fragile" (ibc_fragile i)]

214+-- TODO: Put this back in shortly after minimising/pruning constraints

215+-- makeEntry "ibc_constraints" (ibc_constraints i)]

211216

212217writeArchive :: FilePath -> IBCFile -> Idris ()

213218writeArchive fp i = do let a = L.foldl (\x y -> addEntryToArchive y x) emptyArchive (entries i)

@@ -337,6 +342,7 @@ ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

337342ibc i (IBCAutoHint n h) f = return f { ibc_autohints = (n, h) : ibc_autohints f }

338343ibc i (IBCDeprecate n r) f = return f { ibc_deprecated = (n, r) : ibc_deprecated f }

339344ibc i (IBCFragile n r) f = return f { ibc_fragile = (n,r) : ibc_fragile f }

345+ibc i (IBCConstraint fc u) f = return f { ibc_constraints = (fc, u) : ibc_constraints f }

340346

341347getEntry :: (Binary b, NFData b) => b -> FilePath -> Archive -> Idris b

342348getEntry alt f a = case findEntryByPath f a of

@@ -408,6 +414,7 @@ process reexp phase archive fn = do

408414 processInjective archive

409415 processAccess reexp phase archive

410416 processFragile archive

417+ processConstraints archive

411418

412419timestampOlder :: FilePath -> FilePath -> Idris ()

413420timestampOlder src ibc = do

@@ -462,6 +469,11 @@ processFragile ar = do

462469 ns <- getEntry [] "ibc_fragile" ar

463470 mapM_ (\(n,reason) -> addFragile n reason) ns

464471

472+processConstraints :: Archive -> Idris ()

473+processConstraints ar = do

474+ cs <- getEntry [] "ibc_constraints" ar

475+ mapM_ (\ (fc, c) -> addConstraints fc (0, [c])) cs

476+

465477processImportDirs :: Archive -> Idris ()

466478processImportDirs ar = do

467479 fs <- getEntry [] "ibc_importdirs" ar

src/Idris/Interactive.hs+2−2

@@ -246,8 +246,8 @@ doProofSearch fn updatefile rec l n hints (Just depth)

246246 (ProofSearch rec False depth t psnames hints)]

247247 let def = PClause fc mn (PRef fc [] mn) [] (body top) []

248248 newmv_pre <- idrisCatch

249− (do elabDecl' EAll recinfo (PClauses fc [] mn [def])

250− (tm, ty) <- elabVal recinfo ERHS (PRef fc [] mn)

249+ (do elabDecl' EAll (recinfo (fileFC "proofsearch")) (PClauses fc [] mn [def])

250+ (tm, ty) <- elabVal (recinfo (fileFC "proofsearch")) ERHS (PRef fc [] mn)

251251 ctxt <- getContext

252252 i <- getIState

253253 return . flip displayS "" . renderPretty 1.0 80 $

src/Idris/Parser.hs+2−2

@@ -1804,7 +1804,7 @@ loadSource lidr f toline

18041804 -- we totality check after every Mutual block, so if

18051805 -- anything is a single definition, wrap it in a

18061806 -- mutual block on its own

1807− elabDecls toplevel (map toMutual ds)

1807+ elabDecls (toplevelWith f) (map toMutual ds)

18081808 i <- getIState

18091809 -- simplify every definition do give the totality checker

18101810 -- a better chance

@@ -1883,7 +1883,7 @@ loadSource lidr f toline

18831883 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

18841884 addModDoc syn mname docs =

18851885 do ist <- getIState

1886− docs' <- elabDocTerms recinfo (parsedDocs ist)

1886+ docs' <- elabDocTerms (toplevelWith f) (parsedDocs ist)

18871887 let modDocs' = addDef docName docs' (idris_moduledocs ist)

18881888 putIState ist { idris_moduledocs = modDocs' }

18891889 addIBC (IBCModDocs docName)

src/Idris/Primitives.hs+1−1

@@ -34,7 +34,7 @@ data Prim = Prim { p_name :: Name,

3434

3535ty :: [Const] -> Const -> Type

3636ty [] x = Constant x

37−ty (t:ts) x = Bind (sMN 0 "T") (Pi Nothing (Constant t) (TType (UVar (-3)))) (ty ts x)

37+ty (t:ts) x = Bind (sMN 0 "T") (Pi Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)

3838

3939total, partial, iopartial :: Totality

4040total = Total []

src/Idris/Prover.hs+23−21

@@ -51,13 +51,13 @@ import Util.Pretty

5151import Debug.Trace

5252

5353-- | Launch the proof shell

54−prover :: Bool -> Bool -> Name -> Idris ()

55−prover mode lit x =

54+prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

55+prover info mode lit x =

5656 do ctxt <- getContext

5757 i <- getIState

5858 case lookupTy x ctxt of

5959 [t] -> if elem x (map fst (idris_metavars i))

60− then prove mode (idris_optimisation i) ctxt lit x t

60+ then prove mode info (idris_optimisation i) ctxt lit x t

6161 else ifail $ show x ++ " is not a hole"

6262 _ -> fail "No such hole"

6363

@@ -89,13 +89,13 @@ assumptionNames e

8989 names ((MN _ _, _) : bs) = names bs

9090 names ((n, _) : bs) = show n : names bs

9191

92−prove :: Bool -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

93−prove mode opt ctxt lit n ty

94− = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) (idris_name ist) ty) getIState

92+prove :: Bool -> ElabInfo -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

93+prove mode info opt ctxt lit n ty

94+ = do ps <- fmap (\ist -> initElaborator n (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) ty) getIState

9595 idemodePutSExp "start-proof-mode" n

9696 (tm, prf) <-

9797 if mode

98− then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []

98+ then elabloop info n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []

9999 else do iputStrLn $ "Warning: this interactive prover is deprecated and will be removed " ++

100100 "in a future release. Please see :elab for a similar feature that "++

101101 "will replace it."

@@ -112,7 +112,7 @@ prove mode opt ctxt lit n ty

112112 putIState (i { proof_list = (n, (mode, prf)) : proofs })

113113 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

114114 logLvl 3 (show tree)

115− (ptm, pty) <- recheckC (fileFC "proof") id [] tm

115+ (ptm, pty) <- recheckC (constraintNS info) (fileFC "proof") id [] tm

116116 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

117117 "Expected type:" ++ show ty)

118118 case converts ctxt [] ty pty of

@@ -277,6 +277,8 @@ undoElab prf env st [] = ifail "Nothing to undo"

277277undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h

278278 return (prf', env', st', hs)

279279

280+proverfc = fileFC "prover"

281+

280282runWithInterrupt

281283 :: ElabState EState

282284 -> Idris a -- ^ run with SIGINT handler

@@ -293,8 +295,8 @@ runWithInterrupt elabState mTry mSuccess mFailure = do

293295 if success then mSuccess else mFailure

294296 IdeMode _ _ -> mTry >> mSuccess

295297

296−elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])

297−elabloop fn d prompt prf e prev h env

298+elabloop :: ElabInfo -> Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])

299+elabloop info fn d prompt prf e prev h env

298300 = do ist <- getIState

299301 when d $ dumpState ist True env (proof e)

300302 (x, h') <-

@@ -355,13 +357,13 @@ elabloop fn d prompt prf e prev h env

355357 DoLetP {} -> ifail "Pattern-matching let not supported here"

356358 DoBindP {} -> ifail "Pattern-matching <- not supported here"

357359 DoLet fc i ifc Placeholder expr ->

358− do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

360+ do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)

359361 ctxt <- getContext

360362 let tm' = normaliseAll ctxt [] tm

361363 ty' = normaliseAll ctxt [] ty

362364 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

363365 DoLet fc i ifc ty expr ->

364− do (tm, ty) <- elabVal recinfo ERHS

366+ do (tm, ty) <- elabVal (recinfo proverfc) ERHS

365367 (PApp NoFC (PRef NoFC [] (sUN "the"))

366368 [ pexp (inLets ist env ty)

367369 , pexp (inLets ist env expr)

@@ -371,34 +373,34 @@ elabloop fn d prompt prf e prev h env

371373 ty' = normaliseAll ctxt [] ty

372374 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

373375 DoBind fc i ifc expr ->

374− do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

376+ do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)

375377 (_, e') <- elabStep e saveState -- enable :undo

376378 (res, e'') <- elabStep e' $

377− runElabAction ist NoFC [] tm ["Shell"]

379+ runElabAction info ist NoFC [] tm ["Shell"]

378380 ctxt <- getContext

379381 (v, vty) <- tclift $ check ctxt [] (forget res)

380382 let v' = normaliseAll ctxt [] v

381383 vty' = normaliseAll ctxt [] vty

382384 return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))

383385 DoExp fc expr ->

384− do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

386+ do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)

385387 -- TODO: call elaborator with Elab () as goal here

386388 (_, e') <- elabStep e saveState -- enable :undo

387389 (_, e'') <- elabStep e' $

388− runElabAction ist NoFC [] tm ["Shell"]

390+ runElabAction info ist NoFC [] tm ["Shell"]

389391 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))

390392 (\err -> return (False, prev, e, False, prf, env, Left err))

391393 idemodePutSExp "write-proof-state" (prf', length prf')

392394 case res of

393395 Left err -> do ist <- getIState

394396 iRenderError $ pprintErr ist err

395− elabloop fn d prompt prf' st prev' h' env'

397+ elabloop info fn d prompt prf' st prev' h' env'

396398 Right ok ->

397399 if done then do (tm, _) <- elabStep st get_term

398400 return (tm, prf')

399401 else runWithInterrupt e ok

400− (elabloop fn d prompt prf' st prev' h' env')

401− (elabloop fn d prompt prf e prev h' env)

402+ (elabloop info fn d prompt prf' st prev' h' env')

403+ (elabloop info fn d prompt prf e prev h' env)

402404

403405 where

404406 -- A bit of a hack: wrap the value up in a let binding, which will

@@ -502,7 +504,7 @@ checkType e prf t = do

502504 let OK env = envAtFocus (proof e)

503505 ctxt' = envCtxt env ctxt

504506 putIState ist { tt_ctxt = ctxt' }

505− (tm, ty) <- elabVal recinfo ERHS t

507+ (tm, ty) <- elabVal (recinfo proverfc) ERHS t

506508 let ppo = ppOptionIst ist

507509 ty' = normaliseC ctxt [] ty

508510 infixes = idris_infixes ist

@@ -528,7 +530,7 @@ evalTerm e prf t = withErrorReflection $

528530 ist' = ist { tt_ctxt = ctxt' }

529531 bnd = map (\x -> (fst x, False)) env

530532 putIState ist'

531− (tm, ty) <- elabVal recinfo ERHS t

533+ (tm, ty) <- elabVal (recinfo proverfc) ERHS t

532534 let tm' = force (normaliseAll ctxt' env tm)

533535 ty' = force (normaliseAll ctxt' env ty)

534536 ppo = ppOption (idris_options ist')

src/Idris/REPL.hs+21−20

@@ -836,7 +836,7 @@ process fn (Eval t)

836836 = withErrorReflection $

837837 do logParser 5 $ show t

838838 getIState >>= flip warnDisamb t

839− (tm, ty) <- elabREPL recinfo ERHS t

839+ (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

840840 ctxt <- getContext

841841 let tm' = perhapsForce $ normaliseBlocking ctxt []

842842 [sUN "foreign",

@@ -871,12 +871,12 @@ process fn (NewDefn decls) = do

871871 getClauseName (PWith fc name whole with rhs pn whereBlock) = name

872872 defineName :: [PDecl] -> Idris ()

873873 defineName (tyDecl@(PTy docs argdocs syn fc opts name _ ty) : decls) = do

874− elabDecl EAll recinfo tyDecl

875− elabClauses recinfo fc opts name (concatMap getClauses decls)

874+ elabDecl EAll info tyDecl

875+ elabClauses info fc opts name (concatMap getClauses decls)

876876 setReplDefined (Just name)

877877 defineName [PClauses fc opts _ [clause]] = do

878878 let pterm = getRHS clause

879− (tm,ty) <- elabVal recinfo ERHS pterm

879+ (tm,ty) <- elabVal info ERHS pterm

880880 ctxt <- getContext

881881 let tm' = force (normaliseAll ctxt [] tm)

882882 let ty' = force (normaliseAll ctxt [] ty)

@@ -891,7 +891,7 @@ process fn (NewDefn decls) = do

891891 i <- get

892892 put (addReplSyntax i syntax)

893893 defineName decls = do

894− elabDecls toplevel (map fixClauses decls)

894+ elabDecls (toplevelWith fn) (map fixClauses decls)

895895 setReplDefined (getName (head decls))

896896 getClauses (PClauses fc opts name clauses) = clauses

897897 getClauses _ = []

@@ -915,6 +915,8 @@ process fn (NewDefn decls) = do

915915 fixClauses (PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName decls) =

916916 PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName (map fixClauses decls)

917917 fixClauses decl = decl

918+

919+ info = recinfo (fileFC "toplevel")

918920

919921process fn (Undefine names) = undefine names

920922 where

@@ -954,7 +956,7 @@ process fn (Undefine names) = undefine names

954956process fn (ExecVal t)

955957 = do ctxt <- getContext

956958 ist <- getIState

957− (tm, ty) <- elabVal recinfo ERHS t

959+ (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

958960-- let tm' = normaliseAll ctxt [] tm

959961 let ty' = normaliseAll ctxt [] ty

960962 res <- execute tm

@@ -1001,7 +1003,7 @@ process fn (Check (PRef _ _ n))

10011003

10021004

10031005process fn (Check t)

1004− = do (tm, ty) <- elabREPL recinfo ERHS t

1006+ = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

10051007 ctxt <- getContext

10061008 ist <- getIState

10071009 let ppo = ppOptionIst ist

@@ -1015,7 +1017,7 @@ process fn (Check t)

10151017 (pprintDelab ist ty')

10161018

10171019process fn (Core t)

1018− = do (tm, ty) <- elabREPL recinfo ERHS t

1020+ = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

10191021 iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)

10201022

10211023process fn (DocStr (Left n) w)

@@ -1083,8 +1085,8 @@ process fn (TotCheck n)

10831085 ts

10841086

10851087process fn (DebugUnify l r)

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

1087− (rtm, _) <- elabVal recinfo ERHS r

1088+ = do (ltm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS l

1089+ (rtm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS r

10881090 ctxt <- getContext

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

10901092 OK ans -> iputStrLn (show ans)

@@ -1129,7 +1131,7 @@ process fn (MakeLemma updatefile l n)

11291131process fn (DoProofSearch updatefile rec l n hints)

11301132 = doProofSearch fn updatefile rec l n hints Nothing

11311133process fn (Spec t)

1132− = do (tm, ty) <- elabVal recinfo ERHS t

1134+ = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

11331135 ctxt <- getContext

11341136 ist <- getIState

11351137 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

@@ -1206,22 +1208,21 @@ process fn (Prove mode n')

12061208 [(_, (_,_,_,_,False))] -> ierror (Msg $ "Can't prove this hole as it depends on other holes")

12071209 [(_, (_,_,_,True,_))] -> ierror (Msg $ "Declarations not solvable using prover")

12081210 ns -> ierror (CantResolveAlts (map fst ns))

1209− prover mode (lit fn) n

1211+ prover (toplevelWith fn) mode (lit fn) n

12101212 -- recheck totality

12111213 i <- getIState

12121214 totcheck (fileFC "(input)", n)

12131215 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

12141216 mapM_ checkDeclTotality (idris_totcheck i)

12151217 warnTotality

1216−

12171218process fn (WHNF t)

1218− = do (tm, ty) <- elabVal recinfo ERHS t

1219+ = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

12191220 ctxt <- getContext

12201221 ist <- getIState

12211222 let tm' = whnf ctxt tm

12221223 iPrintResult (show (delab ist tm'))

12231224process fn (TestInline t)

1224− = do (tm, ty) <- elabVal recinfo ERHS t

1225+ = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

12251226 ctxt <- getContext

12261227 ist <- getIState

12271228 let tm' = inlineTerm ist tm

@@ -1230,7 +1231,7 @@ process fn (TestInline t)

12301231process fn (Execute tm)

12311232 = idrisCatch

12321233 (do ist <- getIState

1233− (m, _) <- elabVal recinfo ERHS (elabExec fc tm)

1234+ (m, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS (elabExec fc tm)

12341235 (tmpn, tmph) <- runIO $ tempfile ""

12351236 runIO $ hClose tmph

12361237 t <- codegen

@@ -1253,7 +1254,7 @@ process fn (Compile codegen f)

12531254 let mainname = sNS (sUN "main") ["Main"]

12541255

12551256 m <- if iface then return Nothing else

1256− do (m', _) <- elabVal recinfo ERHS

1257+ do (m', _) <- elabVal (recinfo (fileFC "compiler")) ERHS

12571258 (PApp fc (PRef fc [] (sUN "run__IO"))

12581259 [pexp $ PRef fc [] mainname])

12591260 return (Just m')

@@ -1265,7 +1266,7 @@ process fn (LogLvl i) = setLogLevel i

12651266process fn (LogCategory cs) = setLogCats cs

12661267-- Elaborate as if LHS of a pattern (debug command)

12671268process fn (Pattelab t)

1268− = do (tm, ty) <- elabVal recinfo ELHS t

1269+ = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ELHS t

12691270 iPrintResult $ show tm ++ "\n\n : " ++ show ty

12701271

12711272process fn (Missing n)

@@ -1442,7 +1443,7 @@ process fn (PPrint fmt width (PRef _ _ n))

14421443

14431444

14441445process fn (PPrint fmt width t)

1445− = do (tm, ty) <- elabVal recinfo ERHS t

1446+ = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

14461447 ctxt <- getContext

14471448 ist <- getIState

14481449 let ppo = ppOptionIst ist

@@ -1845,7 +1846,7 @@ execScript expr = do i <- getIState

18451846 Failure err -> do iputStrLn $ show (fixColour c err)

18461847 runIO $ exitWith (ExitFailure 1)

18471848 Success term -> do ctxt <- getContext

1848− (tm, _) <- elabVal recinfo ERHS term

1849+ (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

18491850 res <- execute tm

18501851 runIO $ exitWith ExitSuccess

18511852

src/Idris/Reflection.hs+8−6

@@ -389,8 +389,10 @@ reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

389389reifyTTUExp :: Term -> ElabD UExp

390390reifyTTUExp t@(App _ _ _)

391391 = case unApply t of

392− (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i

393− (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i

392+ (P _ f _, [Constant (Str str), Constant (I i)])

393+ | f == reflm "UVar" -> return $ UVar str i

394+ (P _ f _, [Constant (I i)])

395+ | f == reflm "UVal" -> return $ UVal i

394396 _ -> fail ("Unknown reflection type universe expression: " ++ show t)

395397reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

396398

@@ -792,7 +794,7 @@ reflectConstant WorldType = Var (reflm "WorldType")

792794reflectConstant TheWorld = Var (reflm "TheWorld")

793795

794796reflectUExp :: UExp -> Raw

795−reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]

797+reflectUExp (UVar ns i) = reflCall "UVar" [RConstant (Str ns), RConstant (I i)]

796798reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

797799

798800-- | Reflect the environment of a proof into a List (TTName, Binder TT)

@@ -972,7 +974,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "

972974 Right (TextPart msg)

973975reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

974976 | n == reflm "NamePart" =

975− case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of

977+ case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 Erased) of

976978 Error e -> Left . InternalMsg $

977979 "could not reify name term " ++

978980 show ttn ++

@@ -980,7 +982,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

980982 OK (n', _)-> Right $ NamePart n'

981983reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

982984 | n == reflm "TermPart" =

983− case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of

985+ case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 Erased) of

984986 Error e -> Left . InternalMsg $

985987 "could not reify reflected term " ++

986988 show tm ++

@@ -988,7 +990,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

988990 OK (tm', _) -> Right $ TermPart tm'

989991reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

990992 | n == reflm "RawPart" =

991− case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of

993+ case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 Erased) of

992994 Error e -> Left . InternalMsg $

993995 "could not reify reflected raw term " ++

994996 show tm ++

src/Idris/TypeSearch.hs+1−1

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

436436 unifyQueue state [] = return state

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

438438 --trace ("go: \n" ++ show state) True `seq` return ()

439− res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar 0))) | (n, ty) <- holes state]

439+ res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar [] 0))) | (n, ty) <- holes state]

440440 (ty1, Nothing)

441441 (ty2, Nothing) [] (map fst $ holes state) []

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

test/error001/expected+4−4

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

11test002.idr:1:6:Universe inconsistency.

2− Working on: z

2+ Working on: ./test002.idr.z

33 Old domain: (6,6)

44 New domain: (6,5)

55 Involved constraints:

6− ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}

7− ConstraintFC {uconstraint = y < z, ufc = test002.idr:1:6}

8− ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}

6+ ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}

7+ ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}

8+ ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}

test/interactive010/expected+2−2

@@ -4,9 +4,9 @@ a is not an implicit argument of Prelude.Interfaces./

44Usage is :doc <functionname>

55Usage is :wc <functionname>

66Usage is :printdef <functionname>

7−pat {ty504} : Type u. pat {__class505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__class505}

7+pat {ty504} : Type toplevel.u. pat {__class505} : Prelude.Interfaces.Fractional {ty504}. Prelude.Interfaces./ {ty504} {__class505}

88

9− : pty {ty504} : Type u. pty {__class505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}

9+ : pty {ty504} : Type toplevel.u. pty {__class505} : Prelude.Interfaces.Fractional {ty504}. {ty504} -> {ty504} -> {ty504}

1010(input):1:1: error: expected: ":",

1111 dependent type signature,

1212 end of input

test/quasiquote001/expected+3−3

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

1−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))))

1+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar "./Builtins.idr" 20)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar "./Builtins.idr" 20)))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 25)) (TType (UVar "./Prelude/List.idr" 27))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar "./Builtins.idr" 20)))))

22--------------

3−App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 27))) (TType (UVar 28))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 29))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 23))) (TType (UVar 24))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1))))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1)))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 30))))

3+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar "./QuasiquoteBasics.idr" 27))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 28)) (TType (UVar "./Prelude/List.idr" 30))) (Bind (UN "x") (Pi (V 0) (TType (UVar "./Prelude/List.idr" 31))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar "./Prelude/List.idr" 32))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar "./QuasiquoteBasics.idr" 29))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar "./Prelude/Nat.idr" 20)))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar "./Prelude/Nat.idr" 20))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar "./Prelude/List.idr" 25)) (TType (UVar "./Prelude/List.idr" 27))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar "./QuasiquoteBasics.idr" 30))))

44--------------

5−App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 23))) (TType (UVar 24))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 28))) (TType (UVar 28)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 28))) (TType (UVar 28)))

5+App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (TType (UVar "./QuasiquoteBasics.idr" 28)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar "./Builtins.idr" 74)) (TType (UVar "./Builtins.idr" 76))) (Bind (UN "B") (Pi (TType (UVar "./Builtins.idr" 77)) (TType (UVar "./Builtins.idr" 79))) (Bind (UN "a") (Pi (V 1) (TType (UVar "./Builtins.idr" 80))) (Bind (UN "b") (Pi (V 1) (TType (UVar "./Builtins.idr" 81))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar "./QuasiquoteBasics.idr" 23))) (TType (UVar "./QuasiquoteBasics.idr" 24))) (TType (UVar "./QuasiquoteBasics.idr" 28))) (TType (UVar "./QuasiquoteBasics.idr" 28)))

test/totality014/expected+5−5

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

11totality014.idr:6:9:Universe inconsistency.

2− Working on: u

2+ Working on: ./totality014.idr.u

33 Old domain: (5,5)

44 New domain: (5,4)

55 Involved constraints:

6− ConstraintFC {uconstraint = u <= w, ufc = totality014.idr:6:9}

7− ConstraintFC {uconstraint = u < v, ufc = totality014.idr:1:6}

8− ConstraintFC {uconstraint = w < u, ufc = totality014.idr:1:6}

9− ConstraintFC {uconstraint = u <= w, ufc = totality014.idr:6:9}

6+ ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}

7+ ConstraintFC {uconstraint = ./totality014.idr.u < ./totality014.idr.v, ufc = totality014.idr:1:6}

8+ ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}

9+ ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}

test/universes001/expected+5−5

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

11universes001.idr:7:5:Universe inconsistency.

2− Working on: x

2+ Working on: ./universes001.idr.x

33 Old domain: (5,5)

44 New domain: (5,4)

55 Involved constraints:

6− ConstraintFC {uconstraint = x <= z, ufc = universes001.idr:7:5}

7− ConstraintFC {uconstraint = x < y, ufc = universes001.idr:1:6}

8− ConstraintFC {uconstraint = z < x, ufc = universes001.idr:1:6}

9− ConstraintFC {uconstraint = x <= z, ufc = universes001.idr:7:5}

6+ ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5}

7+ ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6}

8+ ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6}

9+ ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5}

test/universes002/expected+5−5

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

11universes002.idr:45:9:Universe inconsistency.

2− Working on: c7

2+ Working on: ./universes002.idr.c7

33 Old domain: (5,5)

44 New domain: (5,4)

55 Involved constraints:

6− ConstraintFC {uconstraint = c7 <= d1, ufc = universes002.idr:45:9}

7− ConstraintFC {uconstraint = c7 < d7, ufc = universes002.idr:15:6}

8− ConstraintFC {uconstraint = e7 < c7, ufc = universes002.idr:15:6}

9− ConstraintFC {uconstraint = c7 <= d1, ufc = universes002.idr:45:9}

6+ ConstraintFC {uconstraint = ./universes002.idr.c7 <= ./universes002.idr.d1, ufc = universes002.idr:45:9}

7+ ConstraintFC {uconstraint = ./universes002.idr.c7 < ./universes002.idr.d7, ufc = universes002.idr:15:6}

8+ ConstraintFC {uconstraint = ./universes002.idr.e7 < ./universes002.idr.c7, ufc = universes002.idr:15:6}

9+ ConstraintFC {uconstraint = ./universes002.idr.c7 <= ./universes002.idr.d1, ufc = universes002.idr:45:9}