1bd70a1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'ozgurakgun-improve-universe-solver'

1bd70a1Edwin Brady12 years ago

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

compare with master

unifiedsplit

@@ -62,14 +62,34 @@ solve maxUniverseLevel ucs =

62 ]

63 }

65+ lhs (ULT (UVar x) _) = Just (Var x)

66+ lhs (ULE (UVar x) _) = Just (Var x)

67+ lhs _ = Nothing

68+

69+ rhs (ULT _ (UVar x)) = Just (Var x)

70+ rhs (ULE _ (UVar x)) = Just (Var x)

71+ rhs _ = Nothing

72+

65− -- | a map from variables to the list of constraints the variable occurs in.

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

66− constraints :: M.Map Var (S.Set ConstraintFC)

74+ constraintsLHS :: M.Map Var (S.Set ConstraintFC)

67− constraints = M.fromListWith S.union

75+ constraintsLHS = M.fromListWith S.union

68 [ (v, S.singleton (ConstraintFC c fc))

76 [ (v, S.singleton (ConstraintFC c fc))

69− | ConstraintFC c fc <- inpConstraints

77+ | (ConstraintFC c fc) <- inpConstraints

70 , let vars = varsIn c

78 , let vars = varsIn c

71 , length vars > 1 -- do not register unary constraints

79 , length vars > 1 -- do not register unary constraints

72 , v <- vars

80 , v <- vars

81+ , lhs c == Just v

82+ ]

83+

84+ -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)

85+ constraintsRHS :: M.Map Var (S.Set ConstraintFC)

86+ constraintsRHS = M.fromListWith S.union

87+ [ (v, S.singleton (ConstraintFC c fc))

88+ | (ConstraintFC c fc) <- inpConstraints

89+ , let vars = varsIn c

90+ , length vars > 1 -- do not register unary constraints

91+ , v <- vars

92+ , rhs c == Just v

73 ]

93 ]

75 -- | this is where the actual work is done.

95 -- | this is where the actual work is done.

@@ -87,15 +107,15 @@ solve maxUniverseLevel ucs =

87 ULE a b -> do

107 ULE a b -> do

88 Domain lowerA upperA <- domainOf a

108 Domain lowerA upperA <- domainOf a

89 Domain lowerB upperB <- domainOf b

109 Domain lowerB upperB <- domainOf b

90− when (upperB < upperA) $ updateDomainOf (ConstraintFC cons fc) a (Domain lowerA upperB)

110+ when (upperB < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB

91− when (lowerA > lowerB) $ updateDomainOf (ConstraintFC cons fc) b (Domain lowerA upperB)

111+ when (lowerA > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA

92 ULT a b -> do

112 ULT a b -> do

93 Domain lowerA upperA <- domainOf a

113 Domain lowerA upperA <- domainOf a

94 Domain lowerB upperB <- domainOf b

114 Domain lowerB upperB <- domainOf b

95 let upperB_pred = pred upperB

115 let upperB_pred = pred upperB

96 let lowerA_succ = succ lowerA

116 let lowerA_succ = succ lowerA

97− when (upperB_pred < upperA) $ updateDomainOf (ConstraintFC cons fc) a (Domain lowerA upperB_pred)

117+ when (upperB_pred < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB_pred

98− when (lowerA_succ > lowerB) $ updateDomainOf (ConstraintFC cons fc) b (Domain lowerA_succ upperB)

118+ when (lowerA_succ > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA_succ

99 propagate

119 propagate

100

120

101 -- | extract a solution from the state.

121 -- | extract a solution from the state.

@@ -121,12 +141,11 @@ solve maxUniverseLevel ucs =

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

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

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

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

123

143

124− -- | updates the domain of a variable.

125− -- this function is also where we fail, inc ase of a domain wipe-out.

126− updateDomainOf :: ConstraintFC -> UExp -> Domain -> StateT SolverState TC ()

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

127− updateDomainOf suspect (UVar var) newDom = do

145+ updateUpperBoundOf suspect (UVar var) upper = do

128 doms <- gets domainStore

146 doms <- gets domainStore

129− let (oldDom, suspects) = doms M.! Var var

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

148+ let newDom = Domain lower upper

130 when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines

149 when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines

131 $ "Universe inconsistency."

150 $ "Universe inconsistency."

132 : ("Working on: " ++ show (UVar var))

151 : ("Working on: " ++ show (UVar var))

@@ -135,17 +154,48 @@ solve maxUniverseLevel ucs =

135 : "Involved constraints: "

154 : "Involved constraints: "

136 : map (("\t"++) . show) (suspect : S.toList suspects)

155 : map (("\t"++) . show) (suspect : S.toList suspects)

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

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

138− addToQueue (Var var)

157+ addToQueueRHS (uconstraint suspect) (Var var)

139− updateDomainOf _ UVal{} _ = return ()

158+ updateUpperBoundOf _ UVal{} _ = return ()

159+

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

161+ updateLowerBoundOf suspect (UVar var) lower = do

162+ doms <- gets domainStore

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

164+ let newDom = Domain lower upper

165+ when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines

166+ $ "Universe inconsistency."

167+ : ("Working on: " ++ show (UVar var))

168+ : ("Old domain: " ++ show oldDom)

169+ : ("New domain: " ++ show newDom)

170+ : "Involved constraints: "

171+ : map (("\t"++) . show) (suspect : S.toList suspects)

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

173+ addToQueueLHS (uconstraint suspect) (Var var)

174+ updateLowerBoundOf _ UVal{} _ = return ()

175+

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

177+ addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()

178+ addToQueueLHS thisCons var =

179+ case M.lookup var constraintsLHS of

180+ Nothing -> return ()

181+ Just cs -> do

182+ Queue list set <- gets queue

183+ let set' = S.insert thisCons set

184+ let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]

185+ if null newCons

186+ then return ()

187+ else modify $ \ st -> st { queue = Queue (list ++ newCons)

188+ (S.union set (S.fromList (map uconstraint newCons))) }

140

189

141− -- | add all constraints related to a variable.

190+ -- | add all constraints (with the given var on the rhs) to the queue

142− addToQueue :: MonadState SolverState m => Var -> m ()

191+ addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()

143− addToQueue var =

192+ addToQueueRHS thisCons var =

144− case M.lookup var constraints of

193+ case M.lookup var constraintsRHS of

145 Nothing -> return ()

194 Nothing -> return ()

146 Just cs -> do

195 Just cs -> do

147 Queue list set <- gets queue

196 Queue list set <- gets queue

197+ let set' = S.insert thisCons set

148− let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set ]

198+ let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]

149 if null newCons

199 if null newCons

150 then return ()

200 then return ()

151 else modify $ \ st -> st { queue = Queue (list ++ newCons)

201 else modify $ \ st -> st { queue = Queue (list ++ newCons)

src/Idris/Core/Typecheck.hs+35−7

@@ -86,15 +86,38 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

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

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

88 | otherwise = do lift $ tfail $ NoSuchVariable n

89+ chk u env ap@(RApp f RType) | not holes

90+ -- special case to reduce constraintss

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

92+ let fty' = case uniqueBinders (map fst env) (finalise fty) of

93+ ty@(Bind x (Pi i s k) t) -> ty

94+ _ -> uniqueBinders (map fst env)

95+ $ case hnf ctxt env fty of

96+ ty@(Bind x (Pi i s k) t) -> ty

97+ _ -> normalise ctxt env fty

98+ case fty' of

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

100+ do (v, cs) <- get

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

102+ let apty = simplify initContext env

103+ (Bind x (Let (TType v') (TType (UVar v))) t)

104+ return (App fv (TType (UVar v)), apty)

105+ Bind x (Pi i s k) t ->

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

107+ convertsC ctxt env aty s

108+ let apty = simplify initContext env

109+ (Bind x (Let aty av) t)

110+ return (App fv av, apty)

111+ t -> lift $ tfail $ NonFunctionType fv fty

89 chk u env ap@(RApp f a)

112 chk u env ap@(RApp f a)

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

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

91− (av, aty) <- chk u env a

92 let fty' = case uniqueBinders (map fst env) (finalise fty) of

114 let fty' = case uniqueBinders (map fst env) (finalise fty) of

93 ty@(Bind x (Pi i s k) t) -> ty

115 ty@(Bind x (Pi i s k) t) -> ty

94 _ -> uniqueBinders (map fst env)

116 _ -> uniqueBinders (map fst env)

95 $ case hnf ctxt env fty of

117 $ case hnf ctxt env fty of

96 ty@(Bind x (Pi i s k) t) -> ty

118 ty@(Bind x (Pi i s k) t) -> ty

97 _ -> normalise ctxt env fty

119 _ -> normalise ctxt env fty

120+ (av, aty) <- chk u env a

98 case fty' of

121 case fty' of

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

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

100 do convertsC ctxt env aty s

123 do convertsC ctxt env aty s

@@ -135,17 +158,22 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

135 constType TheWorld = Constant WorldType

158 constType TheWorld = Constant WorldType

136 constType Forgot = Erased

159 constType Forgot = Erased

137 constType _ = TType (UVal 0)

160 constType _ = TType (UVal 0)

138− chk u env (RForce t) = do (_, ty) <- chk u env t

161+ chk u env (RForce t)

162+ = do (_, ty) <- chk u env t

139− return (Erased, ty)

163+ return (Erased, ty)

140 chk u env (RBind n (Pi i s k) t)

164 chk u env (RBind n (Pi i s k) t)

141 = do (sv, st) <- chk u env s

165 = do (sv, st) <- chk u env s

142− (kv, kt) <- chk u env k

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

144 (v, cs) <- get

166 (v, cs) <- get

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

168+ put (v+1, cs)

169+ let maxu = UVar v

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

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

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

146 (TType su, TType tu) -> do

172 (TType su, TType tu) -> do

147− when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

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

174+ put (v, ULE su maxu :

175+ ULE tu maxu : cs)

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

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

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

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

150 (pToV n tv), k')

178 (pToV n tv), k')

151 (un, un') ->

179 (un, un') ->

src/Idris/Elab/Data.hs+13−4

@@ -64,7 +64,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

64 = do let codata = Codata `elem` opts

65 iLOG (show fc)

66 undef <- isUndefined fc n

67− (cty, _, t, inacc) <- buildType info syn fc [] n t_in

67+ (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in

68 -- if n is defined already, make sure it is just a type declaration

69 -- with the same type we've just elaborated, and no constructors

70 -- yet

@@ -76,7 +76,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

76 let unique = case getRetTy cty of

77 UType UniqueType -> True

78 _ -> False

79− cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons

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

80 ttag <- getName

81 i <- getIState

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

@@ -210,16 +210,18 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

210 }

211

212elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

213− Type -> -- for kind checking

213+ Type -> -- for unique kind checking

214+ Type -> -- data type's kind

214 (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->

215 (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->

215 Idris (Name, Type)

216 Idris (Name, Type)

216−elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

217+elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)

217 = do checkUndefined fc n

218 = do checkUndefined fc n

218 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

219 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

219 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

220 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

220 ctxt <- getContext

221 ctxt <- getContext

221 let cty' = normalise ctxt [] cty

222 let cty' = normalise ctxt [] cty

222 checkUniqueKind ckind expkind

223 checkUniqueKind ckind expkind

224+ addDataConstraint ckind dkind

223

225

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

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

225 tyIs n cty'

227 tyIs n cty'

@@ -280,6 +282,13 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

280 checkUniqueKind (UType AllTypes) _ = return ()

282 checkUniqueKind (UType AllTypes) _ = return ()

281 checkUniqueKind _ _ = return ()

283 checkUniqueKind _ _ = return ()

282

284

285+ -- Constructor's kind must be <= expected kind

286+ addDataConstraint (TType con) (TType exp)

287+ = do ctxt <- getContext

288+ let v = next_tvar ctxt

289+ addConstraints fc (v, [ULT con exp])

290+ addDataConstraint _ _ = return ()

291+

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

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

284

293

285-- -- Issue #1616 in the issue tracker.

294-- -- Issue #1616 in the issue tracker.

test/error001/expected+7−8

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

1−test002.idr:5:6:Universe inconsistency.

1+test002.idr:1:6:Universe inconsistency.

2−Working on: f2

2+Working on: z

3−Old domain: Domain 7 7

3+Old domain: Domain 6 6

4−New domain: Domain 7 6

4+New domain: Domain 6 5

5Involved constraints:

6− (f2 <= i1,test002.idr:5:6)

6+ ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}

7− (e2 < f2,test002.idr:5:6)

7+ ConstraintFC {uconstraint = y < z, ufc = test002.idr:1:6}

8− (j1 <= f2,test002.idr:5:6)

8+ ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1:6}

9− (f2 <= i1,test002.idr:5:6)

test/quasiquote001/expected+2−2

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

1(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 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 a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 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 a) (Pi (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 a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 32))) (TType (UVar 34))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 36))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (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 a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 38)))))

3+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 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 a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 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))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 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 a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27)))))

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

5−(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32))))

5+(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 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))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 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))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 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))))