4d00ed4 · Idris-dev · git.iko.soy

idris.cabal+7

@@ -873,6 +873,13 @@ Extra-source-files:

873873 test/views003/run

874874 test/views003/*.idr

875875 test/views003/expected

876+

877+ test/universes001/run

878+ test/universes001/*.idr

879+ test/universes001/expected

880+ test/universes002/run

881+ test/universes002/*.idr

882+ test/universes002/expected

876883

877884 test/docs001/run

878885 test/docs001/input

src/Idris/Core/Typecheck.hs+31−24

@@ -58,6 +58,14 @@ 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 =

63+ do (v, cs) <- get

64+ put (v + 1, cs)

65+ case normalise ctxt env tm of

66+ UType _ -> return ()

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

68+

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

6270recheck = recheck_borrowing False []

6371

@@ -175,6 +183,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

175183 put (v+1, cs)

176184 let maxu = UVar v

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

186+

187+-- convertsC ctxt env st (TType maxu)

188+-- convertsC ctxt env tt (TType maxu)

189+-- when holes $ put (v, cs)

190+-- return (Bind n (Pi i (uniqueBinders (map fst env) sv) (TType maxu))

191+-- (pToV n tv), TType maxu)

192+

178193 case (normalise ctxt env st, normalise ctxt env tt) of

179194 (TType su, TType tu) -> do

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

@@ -210,63 +225,55 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

210225 where checkBinder (Lam t)

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

212227 let tv' = normalise ctxt env tv

213− let tt' = normalise ctxt env tt

214− lift $ isType ctxt env tt'

215− return (Lam tv, tt')

228+ convType ctxt env tt

229+ return (Lam tv, tt)

216230 checkBinder (Let t v)

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

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

219233 let tv' = normalise ctxt env tv

220− let tt' = normalise ctxt env tt

221234 convertsC ctxt env vt tv

222− lift $ isType ctxt env tt'

223− return (Let tv vv, tt')

235+ convType ctxt env tt

236+ return (Let tv vv, tt)

224237 checkBinder (NLet t v)

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

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

227240 let tv' = normalise ctxt env tv

228− let tt' = normalise ctxt env tt

229241 convertsC ctxt env vt tv

230− lift $ isType ctxt env tt'

231− return (NLet tv vv, tt')

242+ convType ctxt env tt

243+ return (NLet tv vv, tt)

232244 checkBinder (Hole t)

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

234246 | otherwise

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

236248 let tv' = normalise ctxt env tv

237− let tt' = normalise ctxt env tt

238− lift $ isType ctxt env tt'

239− return (Hole tv, tt')

249+ convType ctxt env tt

250+ return (Hole tv, tt)

240251 checkBinder (GHole i ns t)

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

242253 let tv' = normalise ctxt env tv

243− let tt' = normalise ctxt env tt

244− lift $ isType ctxt env tt'

245− return (GHole i ns tv, tt')

254+ convType ctxt env tt

255+ return (GHole i ns tv, tt)

246256 checkBinder (Guess t v)

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

248258 | otherwise

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

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

251261 let tv' = normalise ctxt env tv

252− let tt' = normalise ctxt env tt

253262 convertsC ctxt env vt tv

254− lift $ isType ctxt env tt'

255− return (Guess tv vv, tt')

263+ convType ctxt env tt

264+ return (Guess tv vv, tt)

256265 checkBinder (PVar t)

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

258267 let tv' = normalise ctxt env tv

259− let tt' = normalise ctxt env tt

260− lift $ isType ctxt env tt'

268+ convType ctxt env tt

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

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

263− return (PVar tv, tt')

271+ return (PVar tv, tt)

264272 checkBinder (PVTy t)

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

266274 let tv' = normalise ctxt env tv

267− let tt' = normalise ctxt env tt

268− lift $ isType ctxt env tt'

269− return (PVTy tv, tt')

275+ convType ctxt env tt

276+ return (PVTy tv, tt)

270277

271278 discharge n (Lam t) bt scv sct

272279 = return (Bind n (Lam t) scv, Bind n (Pi Nothing t bt) sct)

src/Idris/Elab/Data.hs+38−11

@@ -96,10 +96,15 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

9696 rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))

9797 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons

9898 ttag <- getName

99− i <- getIState

10099 let as = map (const (Left (Msg ""))) (getArgTys cty)

101− let params = findParams n (map snd cons)

100+

101+ ctxt <- getContext

102+ let params = findParams n (normalise ctxt [] cty) (map snd cons)

103+

102104 logElab 2 $ "Parameters : " ++ show params

105+ addParamConstraints fc params cty cons

106+

107+ i <- getIState

103108 -- TI contains information about mutually declared types - this will

104109 -- be updated when the mutual block is complete

105110 putIState (i { idris_datatypes =

@@ -143,7 +148,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

143148 (nfc, AnnName n Nothing Nothing Nothing))

144149 dcons

145150 where

146−

147151 checkDefinedAs fc n t i

148152 = let defined = tclift $ tfail (At fc (AlreadyDefined n))

149153 ctxt = tt_ctxt i in

@@ -186,7 +190,6 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

186190 ctxt <- getContext

187191 let cty' = normalise ctxt [] cty

188192 checkUniqueKind ckind expkind

189− addDataConstraint ckind dkind

190193

191194 -- Check that the constructor type is, in fact, a part of the family being defined

192195 tyIs n cty'

@@ -255,13 +258,37 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

255258 checkUniqueKind (UType AllTypes) _

256259 = tclift $ tfail (At fc (UniqueKindError AllTypes n))

257260 checkUniqueKind _ _ = return ()

258−

259− -- Constructor's kind must be <= expected kind

260− addDataConstraint (TType con) (TType exp)

261− = do ctxt <- getContext

262− let v = next_tvar ctxt

263− addConstraints fc (v, [ULT con exp])

264− addDataConstraint _ _ = return ()

261+

262+addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()

263+addParamConstraints fc ps cty cons

264+ = case getRetTy cty of

265+ TType cvar -> mapM_ (addConConstraint ps cvar)

266+ (map getParamNames cons)

267+ _ -> return ()

268+ where

269+ getParamNames (n, ty) = (ty, getPs ty)

270+

271+ getPs (Bind n (Pi _ _ _) sc)

272+ = getPs (substV (P Ref n Erased) sc)

273+ getPs t | (f, args) <- unApply t

274+ = paramArgs 0 args

275+

276+ paramArgs i (P _ n _ : args) | i `elem` ps = n : paramArgs (i + 1) args

277+ paramArgs i (_ : args) = paramArgs (i + 1) args

278+ paramArgs i [] = []

279+

280+ addConConstraint ps cvar (ty, pnames) = constraintTy ty

281+ where

282+ constraintTy (Bind n (Pi _ ty _) sc)

283+ = case getRetTy ty of

284+ TType avar -> do ctxt <- getContext

285+ let tv = next_tvar ctxt

286+ let con = if n `elem` pnames

287+ then ULE avar cvar

288+ else ULT avar cvar

289+ addConstraints fc (tv, [con])

290+ _ -> return ()

291+ constraintTy t = return ()

265292

266293type EliminatorState = StateT (Map.Map String Int) Idris

267294

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

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

27192719 cty (_, _, t) = t

27202720 addIBC (IBCDef tyn)

27212721 mapM_ (addIBC . IBCDef . cn) ctors

2722− let params = findParams tyn (map cty ctors)

2722+ let params = findParams tyn tyconTy (map cty ctors)

27232723 let typeInfo = TI (map cn ctors) False [] params []

27242724 -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.

27252725 -- otherwise writing the IBC just fails silently!

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

@@ -363,14 +363,15 @@ checkVisibility fc n minAcc acc ref

363363-- | Find the type constructor arguments that are parameters, given a

364364-- list of constructor types.

365365--

366−-- Parameters are names which are unchanged across the structure,

367−-- which appear exactly once in the return type of a constructor

368−-- First, find all applications of the constructor, then check over

369−-- them for repeated arguments

366+-- Parameters are names which are unchanged across the structure.

367+-- They appear at least once in every constructor type, always appear

368+-- in the same argument position(s), and nothing else ever appears in those

369+-- argument positions.

370370findParams :: Name -- ^ the name of the family that we are finding parameters for

371+ -> Type -- ^ the type of the type constructor (normalised already)

371372 -> [Type] -- ^ the declared constructor types

372373 -> [Int]

373−findParams tyn ts =

374+findParams tyn famty ts =

374375 let allapps = map getDataApp ts

375376 -- do each constructor separately, then merge the results (names

376377 -- may change between constructors)

@@ -385,9 +386,11 @@ findParams tyn ts =

385386 paramPos [] = []

386387 paramPos (args : rest)

387388 = dropNothing $ keepSame (zip [0..] args) rest

389+

388390 dropNothing [] = []

389391 dropNothing ((x, Nothing) : ts) = dropNothing ts

390392 dropNothing ((x, _) : ts) = x : dropNothing ts

393+

391394 keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->

392395 [(Int, Maybe Name)]

393396 keepSame as [] = as

@@ -398,6 +401,7 @@ findParams tyn ts =

398401 update ((n, Just x) : as) (Just x' : args)

399402 | x == x' = (n, Just x) : update as args

400403 update ((n, _) : as) (_ : args) = (n, Nothing) : update as args

404+

401405 getDataApp :: Type -> [[Maybe Name]]

402406 getDataApp f@(App _ _ _)

403407 | (P _ d _, args) <- unApply f

@@ -405,16 +409,24 @@ findParams tyn ts =

405409 getDataApp (Bind n (Pi _ t _) sc)

406410 = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)

407411 getDataApp _ = []

408− -- keep the arguments which are single names, which don't appear

409− -- elsewhere

412+

413+ -- keep the arguments which are single names, which appear

414+ -- in the return type, counting only the first time they appear in

415+ -- the return type as the parameter position

410416 mParam args [] = []

411417 mParam args (P Bound n _ : rest)

412− | count n args == 1

413− = Just n : mParam args rest

414− where count n [] = 0

415− count n (t : ts)

416− | n `elem` freeNames t = 1 + count n ts

417− | otherwise = count n ts

418+ | paramIn False n args = Just n : mParam (filter (noN n) args) rest

419+ where paramIn ok n [] = ok

420+ paramIn ok n (P _ t _ : ts)

421+ = paramIn (ok || n == t) n ts

422+ paramIn ok n (t : ts)

423+ | n `elem` freeNames t = False -- not a single name

424+ | otherwise = paramIn ok n ts

425+

426+ -- If the name appears again later, don't count that appearance

427+ -- as a parameter position

428+ noN n (P _ t _) = n /= t

429+ noN n _ = False

418430 mParam args (_ : rest) = Nothing : mParam args rest

419431

420432-- | Mark a name as detaggable in the global state (should be called

src/Idris/ElabDecls.hs+12−7

@@ -84,13 +84,18 @@ elabMain = do (m, _) <- elabVal recinfo ERHS

8484

8585-- | Elaborate primitives

8686elabPrims :: Idris ()

87−elabPrims = do mapM_ (elabDecl' EAll recinfo)

88− (map (\(opt, decl, docs, argdocs) -> PData docs argdocs defaultSyntax (fileFC "builtin") opt decl)

89− (zip4

90− [inferOpts, eqOpts]

91− [inferDecl, eqDecl]

92− [emptyDocstring, eqDoc]

93− [[], eqParamDoc]))

87+elabPrims = do i <- getIState

88+ let cs_in = idris_constraints i

89+ let mkdec opt decl docs argdocs =

90+ PData docs argdocs defaultSyntax (fileFC "builtin")

91+ opt decl

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

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

94+ -- it's only scaffolding for the elaborator

95+ i <- getIState

96+ putIState $ i { idris_constraints = cs_in }

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

98+

9499 addNameHint eqTy (sUN "prf")

95100 mapM_ elabPrim primitives

96101 -- Special case prim__believe_me because it doesn't work on just constants

test/proofsearch002/Process.idr−1

@@ -440,4 +440,3 @@ eval st (Loop x) k = eval st x k

440440

441441run : Program a iface -> IO a

442442run p = eval (MkEvalState [] [] 0 0) p (\res, t => pure res)

443−

test/pruviloj001/pruviloj001.idr−1

@@ -68,4 +68,3 @@ appendNilRightId = %runElab mush

6868-- Local Variables:

6969-- idris-load-packages: ("pruviloj")

7070-- End:

71−

test/quasiquote001/expected+2−2

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

11App (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))))))

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 24))) (TType (UVar 25))) (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 26))) (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 22))) (TType (UVar 23))) (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 27))))

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

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 22))) (TType (UVar 23))) (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 22))) (TType (UVar 23))) (TType (UVar 24))) (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 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))

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

test/reg056/reg056.idr−1

@@ -12,4 +12,3 @@ nonk Refl impossible

1212false : Void

1313false = nonk (k Nat Z Z trap Refl)

1414

15−

test/totality014/expected+9−2

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

1−totality014.idr:6:1:

2−Main.runCon2 is possibly not total due to: Main.MkCon2

1+totality014.idr:6:9:Universe inconsistency.

2+ Working on: u

3+ Old domain: (5,5)

4+ New domain: (5,4)

5+ 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}

test/totality014/totality014.idr+1−1

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

11data Con2 : Type where

2− MkCon2 : (a : Type) -> Con2 = a -> (a -> Void) -> Con2

2+ MkCon2 : (a : Type) -> Con2 = a -> (a -> Void) -> Con2

33

44total

55runCon2 : Con2 -> (Con2 -> Void)

test/universes001/expectednew file+9

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

1+universes001.idr:7:5:Universe inconsistency.

2+ Working on: x

3+ Old domain: (5,5)

4+ New domain: (5,4)

5+ 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}

test/universes001/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ universes001.idr --check

3+rm -f *.ibc

test/universes001/universes001.idrnew file+8

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

1+data Exp : Type -> Type where

2+ Const : {t : Type} -> t -> Exp t

3+ Pair : {t1,t2:Type} -> Exp t1 -> Exp t2 -> Exp (t1, t2)

4+ Eq : {t:Type} -> Exp t -> Exp t -> Exp Bool

5+

6+foo : Exp (Exp Integer)

7+foo = Const (Const 0)

8+

test/universes002/expectednew file+9

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

1+universes002.idr:45:9:Universe inconsistency.

2+ Working on: c7

3+ Old domain: (5,5)

4+ New domain: (5,4)

5+ 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}

test/universes002/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ universes002.idr --check

3+rm -f *.ibc

test/universes002/universes002.idrnew file+45

@@ -0,0 +1,45 @@

1+module TypeInType

2+

3+data MPair : (a : Type) -> (P : a -> Type) -> Type where

4+ MkMPair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> MPair a P

5+

6+data EQt : a -> b -> Type where

7+ REFL : EQt x x

8+

9+msym : EQt x y -> EQt y x

10+msym REFL = REFL

11+

12+mreplace : {a,x,y:_} -> {P : a -> Type} -> EQt x y -> P x -> P y

13+mreplace REFL p = p

14+

15+data Tree : Type where

16+ Sup : (a : Type) -> (f : a -> Tree) -> Tree

17+

18+A : Tree -> Type

19+A (Sup a _) = a

20+

21+F : (t : Tree) -> A t -> Tree

22+F (Sup a f) = f

23+

24+normal : Tree -> Type

25+normal t = (MPair (A t) (\y => EQt (F t y) (Sup (A t) (F t)))) -> Void

26+

27+NT : Type

28+NT = MPair Tree (\t => normal t)

29+

30+p : NT -> Tree

31+p (MkMPair x _) = x

32+

33+R : Tree

34+R = Sup NT p

35+

36+lemma : normal R

37+lemma (MkMPair (MkMPair y1 y2) z)

38+ = y2

39+ (mreplace {P = (\ y3 => (MPair (A y3)

40+ (\y => EQt (F y3 y) (Sup (A y3) (F y3)))))}

41+ (msym z) (MkMPair (MkMPair y1 y2) z))

42+

43+total

44+russell : Void

45+russell = lemma (MkMPair (MkMPair R lemma) REFL)