cef8780 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix constraint generation/tests

cef8780Edwin Brady12 years ago

src/Idris/Core/Typecheck.hs+36−40

compare with master

unifiedsplit

@@ -69,7 +69,7 @@ check ctxt env tm

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

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

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

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

74 smaller (UType NullType) _ = UType NullType

75 smaller _ (UType NullType) = UType NullType

@@ -78,18 +78,17 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where

78 smaller x _ = x

80 chk :: Type -> -- uniqueness level

81− Maybe UExp -> -- maximum universe level, if known

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

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

83− chk u maxu env (Var n)

82+ chk u env (Var n)

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

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

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

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

86 -- checking an already elaborated term, we do

85 -- checking an already elaborated term, we do

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

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

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

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

89 | otherwise = do lift $ tfail $ NoSuchVariable n

88 | otherwise = do lift $ tfail $ NoSuchVariable n

90− chk u maxu env ap@(RApp f RType) | not holes

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

91 -- special case to reduce constraintss

90 -- special case to reduce constraintss

92− = do (fv, fty) <- chk u maxu env f

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

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

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

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

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

95 _ -> uniqueBinders (map fst env)

94 _ -> uniqueBinders (map fst env)

@@ -104,21 +103,21 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where

104 (Bind x (Let (TType v') (TType (UVar v))) t)

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

105 return (App fv (TType (UVar v)), apty)

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

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

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

107− do (av, aty) <- chk u maxu env RType

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

108 convertsC ctxt env aty s

107 convertsC ctxt env aty s

109 let apty = simplify initContext env

108 let apty = simplify initContext env

110 (Bind x (Let aty av) t)

109 (Bind x (Let aty av) t)

111 return (App fv av, apty)

110 return (App fv av, apty)

112 t -> lift $ tfail $ NonFunctionType fv fty

111 t -> lift $ tfail $ NonFunctionType fv fty

113− chk u maxu env ap@(RApp f a)

112+ chk u env ap@(RApp f a)

114− = do (fv, fty) <- chk u maxu env f

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

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

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

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

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

117 _ -> uniqueBinders (map fst env)

116 _ -> uniqueBinders (map fst env)

118 $ case hnf ctxt env fty of

117 $ case hnf ctxt env fty of

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

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

120 _ -> normalise ctxt env fty

119 _ -> normalise ctxt env fty

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

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

122 case fty' of

121 case fty' of

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

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

124 do convertsC ctxt env aty s

123 do convertsC ctxt env aty s

@@ -126,13 +125,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where

126 (Bind x (Let aty av) t)

125 (Bind x (Let aty av) t)

127 return (App fv av, apty)

126 return (App fv av, apty)

128 t -> lift $ tfail $ NonFunctionType fv fty

127 t -> lift $ tfail $ NonFunctionType fv fty

129− chk u maxu env RType

128+ chk u env RType

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

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

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

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

132 let c = ULT (UVar v) (UVar (v+1))

131 let c = ULT (UVar v) (UVar (v+1))

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

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

134 return (TType (UVar v), TType (UVar (v+1)))

133 return (TType (UVar v), TType (UVar (v+1)))

135− chk u maxu env (RUType un)

134+ chk u env (RUType un)

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

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

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

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

138 -- https://github.com/idris-lang/Idris-dev/issues/1715

137 -- https://github.com/idris-lang/Idris-dev/issues/1715

@@ -141,8 +140,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where

141 -- put (v+2, (c:cs))

140 -- put (v+2, (c:cs))

142 -- return (TType (UVar v), TType (UVar (v+1)))

141 -- return (TType (UVar v), TType (UVar (v+1)))

143 return (UType un, TType (UVal 0))

142 return (UType un, TType (UVal 0))

144− chk u maxu env (RConstant Forgot) = return (Erased, Erased)

143+ chk u env (RConstant Forgot) = return (Erased, Erased)

145− chk u maxu env (RConstant c) = return (Constant c, constType c)

144+ chk u env (RConstant c) = return (Constant c, constType c)

146 where constType (I _) = Constant (AType (ATInt ITNative))

145 where constType (I _) = Constant (AType (ATInt ITNative))

147 constType (BI _) = Constant (AType (ATInt ITBig))

146 constType (BI _) = Constant (AType (ATInt ITBig))

148 constType (Fl _) = Constant (AType ATFloat)

147 constType (Fl _) = Constant (AType ATFloat)

@@ -159,24 +158,21 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where

159 constType TheWorld = Constant WorldType

158 constType TheWorld = Constant WorldType

160 constType Forgot = Erased

159 constType Forgot = Erased

161 constType _ = TType (UVal 0)

160 constType _ = TType (UVal 0)

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

161+ chk u env (RForce t)

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

163− return (Erased, ty)

163+ return (Erased, ty)

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

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

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

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

166− vcs <- get

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

168− put vcs -- no need to validate these constraints, they are independent

169 (v, cs) <- get

166 (v, cs) <- get

170− nmaxu <- case maxu of

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

171− Nothing -> do put (v+1, cs)

168+ put (v+1, cs)

172− return (UVar v)

169+ let maxu = UVar v

173− Just m -> return m

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

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

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

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

176 (TType su, TType tu) -> do

172 (TType su, TType tu) -> do

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

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

178− put (v, ULE su nmaxu :

174+ put (v, ULE su maxu :

179− ULE tu nmaxu : cs)

175+ ULE tu maxu : cs)

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

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

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

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

182 (pToV n tv), k')

178 (pToV n tv), k')

@@ -200,27 +196,27 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where

200 mostUnique (Pi _ _ pk : es) k = mostUnique es (smaller pk k)

196 mostUnique (Pi _ _ pk : es) k = mostUnique es (smaller pk k)

201 mostUnique (_ : es) k = mostUnique es k

197 mostUnique (_ : es) k = mostUnique es k

202

198

203− chk u maxu env (RBind n b sc)

199+ chk u env (RBind n b sc)

204 = do (b', bt') <- checkBinder b

200 = do (b', bt') <- checkBinder b

205− (scv, sct) <- chk (smaller bt' u) maxu ((n, b'):env) sc

201+ (scv, sct) <- chk (smaller bt' u) ((n, b'):env) sc

206 discharge n b' bt' (pToV n scv) (pToV n sct)

202 discharge n b' bt' (pToV n scv) (pToV n sct)

207 where checkBinder (Lam t)

203 where checkBinder (Lam t)

208− = do (tv, tt) <- chk u maxu env t

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

209 let tv' = normalise ctxt env tv

205 let tv' = normalise ctxt env tv

210 let tt' = normalise ctxt env tt

206 let tt' = normalise ctxt env tt

211 lift $ isType ctxt env tt'

207 lift $ isType ctxt env tt'

212 return (Lam tv, tt')

208 return (Lam tv, tt')

213 checkBinder (Let t v)

209 checkBinder (Let t v)

214− = do (tv, tt) <- chk u maxu env t

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

215− (vv, vt) <- chk u maxu env v

211+ (vv, vt) <- chk u env v

216 let tv' = normalise ctxt env tv

212 let tv' = normalise ctxt env tv

217 let tt' = normalise ctxt env tt

213 let tt' = normalise ctxt env tt

218 convertsC ctxt env vt tv

214 convertsC ctxt env vt tv

219 lift $ isType ctxt env tt'

215 lift $ isType ctxt env tt'

220 return (Let tv vv, tt')

216 return (Let tv vv, tt')

221 checkBinder (NLet t v)

217 checkBinder (NLet t v)

222− = do (tv, tt) <- chk u maxu env t

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

223− (vv, vt) <- chk u maxu env v

219+ (vv, vt) <- chk u env v

224 let tv' = normalise ctxt env tv

220 let tv' = normalise ctxt env tv

225 let tt' = normalise ctxt env tt

221 let tt' = normalise ctxt env tt

226 convertsC ctxt env vt tv

222 convertsC ctxt env vt tv

@@ -229,13 +225,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where

229 checkBinder (Hole t)

225 checkBinder (Hole t)

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

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

231 | otherwise

227 | otherwise

232− = do (tv, tt) <- chk u maxu env t

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

233 let tv' = normalise ctxt env tv

229 let tv' = normalise ctxt env tv

234 let tt' = normalise ctxt env tt

230 let tt' = normalise ctxt env tt

235 lift $ isType ctxt env tt'

231 lift $ isType ctxt env tt'

236 return (Hole tv, tt')

232 return (Hole tv, tt')

237 checkBinder (GHole i t)

233 checkBinder (GHole i t)

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

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

239 let tv' = normalise ctxt env tv

235 let tv' = normalise ctxt env tv

240 let tt' = normalise ctxt env tt

236 let tt' = normalise ctxt env tt

241 lift $ isType ctxt env tt'

237 lift $ isType ctxt env tt'

@@ -243,15 +239,15 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where

243 checkBinder (Guess t v)

239 checkBinder (Guess t v)

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

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

245 | otherwise

241 | otherwise

246− = do (tv, tt) <- chk u maxu env t

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

247− (vv, vt) <- chk u maxu env v

243+ (vv, vt) <- chk u env v

248 let tv' = normalise ctxt env tv

244 let tv' = normalise ctxt env tv

249 let tt' = normalise ctxt env tt

245 let tt' = normalise ctxt env tt

250 convertsC ctxt env vt tv

246 convertsC ctxt env vt tv

251 lift $ isType ctxt env tt'

247 lift $ isType ctxt env tt'

252 return (Guess tv vv, tt')

248 return (Guess tv vv, tt')

253 checkBinder (PVar t)

249 checkBinder (PVar t)

254− = do (tv, tt) <- chk u maxu env t

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

255 let tv' = normalise ctxt env tv

251 let tv' = normalise ctxt env tv

256 let tt' = normalise ctxt env tt

252 let tt' = normalise ctxt env tt

257 lift $ isType ctxt env tt'

253 lift $ isType ctxt env tt'

@@ -259,7 +255,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where

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

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

260 return (PVar tv, tt')

256 return (PVar tv, tt')

261 checkBinder (PVTy t)

257 checkBinder (PVTy t)

262− = do (tv, tt) <- chk u maxu env t

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

263 let tv' = normalise ctxt env tv

259 let tv' = normalise ctxt env tv

264 let tt' = normalise ctxt env tt

260 let tt' = normalise ctxt env tt

265 lift $ isType ctxt env tt'

261 lift $ isType ctxt env tt'

test/error001/expected+4−4

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

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

2−Working on: t

2+Working on: z

3Old domain: Domain 6 6

4New domain: Domain 6 5

5Involved constraints:

6− ConstraintFC {uconstraint = t <= u, ufc = test002.idr:1:6}

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

7− ConstraintFC {uconstraint = s < t, ufc = test002.idr:1:6}

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

8− ConstraintFC {uconstraint = t <= u, ufc = test002.idr:1:6}

8+ ConstraintFC {uconstraint = z <= a1, ufc = test002.idr:1: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))))