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

idris.cabal+7

compare with master

unifiedsplit

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

873 test/views003/run

874 test/views003/*.idr

875 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

876

883

877 test/docs001/run

884 test/docs001/run

878 test/docs001/input

885 test/docs001/input

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

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

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

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

60

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+

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

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

62recheck = recheck_borrowing False []

70recheck = recheck_borrowing False []

63

71

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

175 put (v+1, cs)

183 put (v+1, cs)

176 let maxu = UVar v

184 let maxu = UVar v

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

185 (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+

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

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

179 (TType su, TType tu) -> do

194 (TType su, TType tu) -> do

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

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

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

210 where checkBinder (Lam t)

225 where checkBinder (Lam t)

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

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

212 let tv' = normalise ctxt env tv

227 let tv' = normalise ctxt env tv

213− let tt' = normalise ctxt env tt

214− lift $ isType ctxt env tt'

228+ convType ctxt env tt

215− return (Lam tv, tt')

229+ return (Lam tv, tt)

216 checkBinder (Let t v)

230 checkBinder (Let t v)

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

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

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

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

219 let tv' = normalise ctxt env tv

233 let tv' = normalise ctxt env tv

220− let tt' = normalise ctxt env tt

221 convertsC ctxt env vt tv

234 convertsC ctxt env vt tv

222− lift $ isType ctxt env tt'

235+ convType ctxt env tt

223− return (Let tv vv, tt')

236+ return (Let tv vv, tt)

224 checkBinder (NLet t v)

237 checkBinder (NLet t v)

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

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

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

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

227 let tv' = normalise ctxt env tv

240 let tv' = normalise ctxt env tv

228− let tt' = normalise ctxt env tt

229 convertsC ctxt env vt tv

241 convertsC ctxt env vt tv

230− lift $ isType ctxt env tt'

242+ convType ctxt env tt

231− return (NLet tv vv, tt')

243+ return (NLet tv vv, tt)

232 checkBinder (Hole t)

244 checkBinder (Hole t)

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

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

234 | otherwise

246 | otherwise

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

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

236 let tv' = normalise ctxt env tv

248 let tv' = normalise ctxt env tv

237− let tt' = normalise ctxt env tt

238− lift $ isType ctxt env tt'

249+ convType ctxt env tt

239− return (Hole tv, tt')

250+ return (Hole tv, tt)

240 checkBinder (GHole i ns t)

251 checkBinder (GHole i ns t)

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

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

242 let tv' = normalise ctxt env tv

253 let tv' = normalise ctxt env tv

243− let tt' = normalise ctxt env tt

244− lift $ isType ctxt env tt'

254+ convType ctxt env tt

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

255+ return (GHole i ns tv, tt)

246 checkBinder (Guess t v)

256 checkBinder (Guess t v)

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

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

248 | otherwise

258 | otherwise

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

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

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

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

251 let tv' = normalise ctxt env tv

261 let tv' = normalise ctxt env tv

252− let tt' = normalise ctxt env tt

253 convertsC ctxt env vt tv

262 convertsC ctxt env vt tv

254− lift $ isType ctxt env tt'

263+ convType ctxt env tt

255− return (Guess tv vv, tt')

264+ return (Guess tv vv, tt)

256 checkBinder (PVar t)

265 checkBinder (PVar t)

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

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

258 let tv' = normalise ctxt env tv

267 let tv' = normalise ctxt env tv

259− let tt' = normalise ctxt env tt

260− lift $ isType ctxt env tt'

268+ convType ctxt env tt

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

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

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

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

263− return (PVar tv, tt')

271+ return (PVar tv, tt)

264 checkBinder (PVTy t)

272 checkBinder (PVTy t)

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

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

266 let tv' = normalise ctxt env tv

274 let tv' = normalise ctxt env tv

267− let tt' = normalise ctxt env tt

268− lift $ isType ctxt env tt'

275+ convType ctxt env tt

269− return (PVTy tv, tt')

276+ return (PVTy tv, tt)

270

277

271 discharge n (Lam t) bt scv sct

278 discharge n (Lam t) bt scv sct

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

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

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

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

98 ttag <- getName

99− i <- getIState

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

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

100+

101+ ctxt <- getContext

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

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

103+

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

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

105+ addParamConstraints fc params cty cons

106+

107+ i <- getIState

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

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

104 -- be updated when the mutual block is complete

109 -- be updated when the mutual block is complete

105 putIState (i { idris_datatypes =

110 putIState (i { idris_datatypes =

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

143 (nfc, AnnName n Nothing Nothing Nothing))

148 (nfc, AnnName n Nothing Nothing Nothing))

144 dcons

149 dcons

145 where

150 where

146−

147 checkDefinedAs fc n t i

151 checkDefinedAs fc n t i

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

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

149 ctxt = tt_ctxt i in

153 ctxt = tt_ctxt i in

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

186 ctxt <- getContext

190 ctxt <- getContext

187 let cty' = normalise ctxt [] cty

191 let cty' = normalise ctxt [] cty

188 checkUniqueKind ckind expkind

192 checkUniqueKind ckind expkind

189− addDataConstraint ckind dkind

190

193

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

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

192 tyIs n cty'

195 tyIs n cty'

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

255 checkUniqueKind (UType AllTypes) _

258 checkUniqueKind (UType AllTypes) _

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

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

257 checkUniqueKind _ _ = return ()

260 checkUniqueKind _ _ = return ()

258−

261+

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

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

260− addDataConstraint (TType con) (TType exp)

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

261− = do ctxt <- getContext

284+ TType avar -> do ctxt <- getContext

262− let v = next_tvar ctxt

285+ let tv = next_tvar ctxt

286+ let con = if n `elem` pnames

287+ then ULE avar cvar

288+ else ULT avar cvar

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

289+ addConstraints fc (tv, [con])

264− addDataConstraint _ _ = return ()

290+ _ -> return ()

291+ constraintTy t = return ()

265

292

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

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

267

294

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

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

2719 cty (_, _, t) = t

2720 addIBC (IBCDef tyn)

2721 mapM_ (addIBC . IBCDef . cn) ctors

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

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

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

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

2725 -- otherwise writing the IBC just fails silently!

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

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

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

364-- list of constructor types.

365--

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

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

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

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

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

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

369−-- them for repeated arguments

369+-- argument positions.

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

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

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

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

372 -> [Int]

373 -> [Int]

373−findParams tyn ts =

374+findParams tyn famty ts =

374 let allapps = map getDataApp ts

375 let allapps = map getDataApp ts

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

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

376 -- may change between constructors)

377 -- may change between constructors)

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

385 paramPos [] = []

386 paramPos [] = []

386 paramPos (args : rest)

387 paramPos (args : rest)

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

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

389+

388 dropNothing [] = []

390 dropNothing [] = []

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

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

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

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

393+

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

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

392 [(Int, Maybe Name)]

395 [(Int, Maybe Name)]

393 keepSame as [] = as

396 keepSame as [] = as

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

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

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

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

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

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

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

404+

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

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

402 getDataApp f@(App _ _ _)

406 getDataApp f@(App _ _ _)

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

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

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

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

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

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

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

407 getDataApp _ = []

411 getDataApp _ = []

412+

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

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

409− -- elsewhere

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

415+ -- the return type as the parameter position

410 mParam args [] = []

416 mParam args [] = []

411 mParam args (P Bound n _ : rest)

417 mParam args (P Bound n _ : rest)

412− | count n args == 1

413− = Just n : mParam args rest

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

414− where count n [] = 0

419+ where paramIn ok n [] = ok

415− count n (t : ts)

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

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

422+ paramIn ok n (t : ts)

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

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

417− | otherwise = count n ts

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

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

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

419

431

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

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

84

85-- | Elaborate primitives

86elabPrims :: Idris ()

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

87+elabPrims = do i <- getIState

88+ let cs_in = idris_constraints i

89+ let mkdec opt decl docs argdocs =

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

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

89− (zip4

91+ opt decl

90− [inferOpts, eqOpts]

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

91− [inferDecl, eqDecl]

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

92− [emptyDocstring, eqDoc]

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

93− [[], eqParamDoc]))

95+ i <- getIState

96+ putIState $ i { idris_constraints = cs_in }

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

98+

94 addNameHint eqTy (sUN "prf")

99 addNameHint eqTy (sUN "prf")

95 mapM_ elabPrim primitives

100 mapM_ elabPrim primitives

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

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

440

441run : Program a iface -> IO a

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

443−

test/pruviloj001/pruviloj001.idr−1

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

68-- Local Variables:

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

70-- End:

71−

test/quasiquote001/expected+2−2

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

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

2--------------

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

4--------------

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

12false : Void

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

14

15−

test/totality014/expected+9−2

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

1−totality014.idr:6:1:

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

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

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

1data Con2 : Type where

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

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

3

4total

5runCon2 : 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)