summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPéter Diviánszky <divipp@gmail.com>2016-02-02 06:19:58 +0100
committerPéter Diviánszky <divipp@gmail.com>2016-02-02 06:19:58 +0100
commit0134e614c1747d2d9aff56f260249d809b541287 (patch)
treebe372f350f8cec8abea24ef438481ecccae8eb47
parentc5d17f3b0db34216d9ce4884b4a0ae044ee57257 (diff)
try to speed up parseTerm
-rw-r--r--lc/Internals.lc2
-rw-r--r--src/LambdaCube/Compiler/Lexer.hs12
-rw-r--r--src/LambdaCube/Compiler/Parser.hs29
-rw-r--r--testdata/Builtins.out92
-rw-r--r--testdata/Internals.out254
-rw-r--r--testdata/Prelude.out2
-rw-r--r--testdata/language-features/basic-values/def05.reject.out2
-rw-r--r--testdata/language-features/basic-values/def06.reject.out2
-rw-r--r--testdata/language-features/basic-values/redefine03.reject.out2
-rw-r--r--testdata/language-features/guard/guard10.reject.out2
-rw-r--r--testdata/listcompr01.reject.out2
11 files changed, 248 insertions, 153 deletions
diff --git a/lc/Internals.lc b/lc/Internals.lc
index df5814e6..0ea96032 100644
--- a/lc/Internals.lc
+++ b/lc/Internals.lc
@@ -41,6 +41,8 @@ type family T2 a b
41-- equality constraints 41-- equality constraints
42type family EqCT (t :: Type) (a :: t) (b :: t) 42type family EqCT (t :: Type) (a :: t) (b :: t)
43 43
44type EqCTt = EqCT Type
45
44--type instance EqCT t (a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b') 46--type instance EqCT t (a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b')
45 47
46-- builtin conjuction of constraint witnesses 48-- builtin conjuction of constraint witnesses
diff --git a/src/LambdaCube/Compiler/Lexer.hs b/src/LambdaCube/Compiler/Lexer.hs
index 9bf3dc8c..171dd5cf 100644
--- a/src/LambdaCube/Compiler/Lexer.hs
+++ b/src/LambdaCube/Compiler/Lexer.hs
@@ -42,12 +42,10 @@ import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens)
42-- see http://blog.ezyang.com/2014/05/parsec-try-a-or-b-considered-harmful/comment-page-1/#comment-6602 42-- see http://blog.ezyang.com/2014/05/parsec-try-a-or-b-considered-harmful/comment-page-1/#comment-6602
43try_ s m = Pa.try m <?> s 43try_ s m = Pa.try m <?> s
44 44
45-- n, m >= 1, n < m 45manyNM a b _ | b < a || b < 0 || a < 0 = mzero
46manyNM n m p = do 46manyNM 0 0 _ = pure []
47 xs <- many1 p 47manyNM 0 n p = option [] $ (:) <$> p <*> manyNM 0 (n-1) p
48 let lxs = length xs 48manyNM k n p = (:) <$> p <*> manyNM (k-1) (n-1) p
49 unless (n <= lxs && lxs <= m) . fail $ unwords ["manyNM", show n, show m, "found", show lxs, "occurences."]
50 return xs
51 49
52-------------------------------------------------------------------------------- parser type 50-------------------------------------------------------------------------------- parser type
53 51
@@ -262,7 +260,7 @@ calcPrec
262 -> e 260 -> e
263 -> [(f, e)] 261 -> [(f, e)]
264 -> e 262 -> e
265calcPrec app getFixity e = compileOps [((Infix, -1), undefined, e)] 263calcPrec app getFixity e = compileOps [((Infix, -1000), error "calcPrec", e)]
266 where 264 where
267 compileOps [(_, _, e)] [] = e 265 compileOps [(_, _, e)] [] = e
268 compileOps acc [] = compileOps (shrink acc) [] 266 compileOps acc [] = compileOps (shrink acc) []
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 74f7d3d0..2becb86c 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -351,7 +351,8 @@ parseETerm = expNS . parseTerm
351parseTerm :: Prec -> P SExp 351parseTerm :: Prec -> P SExp
352parseTerm prec = withRange setSI $ case prec of 352parseTerm prec = withRange setSI $ case prec of
353 PrecLam -> 353 PrecLam ->
354 mkIf <$ reserved "if" <*> parseTerm PrecLam <* reserved "then" <*> parseTerm PrecLam <* reserved "else" <*> parseTerm PrecLam 354 do level PrecAnn $ \t -> mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> parseTTerm PrecLam
355 <|> mkIf <$ reserved "if" <*> parseTerm PrecLam <* reserved "then" <*> parseTerm PrecLam <* reserved "else" <*> parseTerm PrecLam
355 <|> do reserved "forall" 356 <|> do reserved "forall"
356 (fe, ts) <- telescope (Just $ Wildcard SType) 357 (fe, ts) <- telescope (Just $ Wildcard SType)
357 f <- SPi . const Hidden <$ reservedOp "." <|> SPi . const Visible <$ reservedOp "->" 358 f <- SPi . const Hidden <$ reservedOp "." <|> SPi . const Visible <$ reservedOp "->"
@@ -363,21 +364,17 @@ parseTerm prec = withRange setSI $ case prec of
363 t' <- dbf' fe <$> parseTerm PrecLam 364 t' <- dbf' fe <$> parseTerm PrecLam
364 ge <- dsInfo 365 ge <- dsInfo
365 return $ foldr (uncurry (patLam_ id ge)) t' ts 366 return $ foldr (uncurry (patLam_ id ge)) t' ts
366 <|> compileCase <$> dsInfo 367 <|> compileCase <$ reserved "case" <*> dsInfo <*> parseETerm PrecLam <* reserved "of" <*> do
367 <* reserved "case" <*> parseETerm PrecLam 368 localIndentation Ge $ localAbsoluteIndentation $ some $ do
368 <* reserved "of" <*> do 369 (fe, p) <- longPattern
369 localIndentation Ge $ localAbsoluteIndentation $ some $ do 370 (,) p <$> parseRHS (dbf' fe) "->"
370 (fe, p) <- longPattern 371-- <|> compileGuardTree id id <$> dsInfo <*> (Alts <$> parseSomeGuards (const True))
371 (,) p <$> parseRHS (dbf' fe) "->"
372 <|> compileGuardTree id id <$> dsInfo <*> (Alts <$> parseSomeGuards (const True))
373 <|> do level PrecEq $ \t -> mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> parseTTerm PrecLam
374 PrecEq -> level PrecAnn $ \t -> SAppV (SBuiltin "'EqCT" `SAppV` SType `SAppV` t) <$ reservedOp "~" <*> parseTTerm PrecAnn
375 PrecAnn -> level PrecOp $ \t -> SAnn t <$> parseType Nothing 372 PrecAnn -> level PrecOp $ \t -> SAnn t <$> parseType Nothing
376 PrecOp -> join $ calculatePrecs <$> namespace <*> dsInfo <*> (notExp <|> notOp False) where 373 PrecOp -> (notOp False <|> notExp) >>= \xs -> join $ calculatePrecs <$> namespace <*> dsInfo <*> pure xs where
377 notExp = (++) <$> ope <*> notOp True 374 notExp = (++) <$> ope <*> notOp True
378 notOp x = (++) <$> try "expression" ((++) <$> ex PrecApp <*> option [] ope) <*> notOp True 375 notOp x = (++) <$> try "expression" ((++) <$> ex PrecApp <*> option [] ope) <*> notOp True
379 <|> if x then option [] (try "lambda" $ ex PrecLam) else mzero 376 <|> if x then option [] (try "lambda" $ ex PrecLam) else mzero
380 ope = pure . Left <$> parseSIName operatorT 377 ope = pure . Left <$> parseSIName (operatorT <|> "'EqCTt" <$ reservedOp "~")
381 ex pr = pure . Right <$> parseTerm pr 378 ex pr = pure . Right <$> parseTerm pr
382 PrecApp -> 379 PrecApp ->
383 apps' <$> try "record" (sVar upperCase <* reservedOp "{") <*> (commaSep $ lowerCase *> reservedOp "=" *> ((,) Visible <$> parseTerm PrecLam)) <* reservedOp "}" 380 apps' <$> try "record" (sVar upperCase <* reservedOp "{") <*> (commaSep $ lowerCase *> reservedOp "=" *> ((,) Visible <$> parseTerm PrecLam)) <* reservedOp "}"
@@ -805,7 +802,7 @@ parseDef =
805 cs <- option [] $ reserved "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ typedIds Nothing) 802 cs <- option [] $ reserved "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ typedIds Nothing)
806 return $ pure $ Class x (map snd ts) (concatMap (\(vs, t) -> (,) <$> vs <*> pure (dbf' nps t)) cs) 803 return $ pure $ Class x (map snd ts) (concatMap (\(vs, t) -> (,) <$> vs <*> pure (dbf' nps t)) cs)
807 <|> do indentation (reserved "instance") $ typeNS $ do 804 <|> do indentation (reserved "instance") $ typeNS $ do
808 constraints <- option [] $ try "constraint" $ getTTuple' <$> parseTerm PrecEq <* reservedOp "=>" 805 constraints <- option [] $ try "constraint" $ getTTuple' <$> parseTerm PrecOp <* reservedOp "=>"
809 x <- parseSIName upperCase 806 x <- parseSIName upperCase
810 (nps, args) <- telescopePat 807 (nps, args) <- telescopePat
811 checkPattern nps 808 checkPattern nps
@@ -885,9 +882,9 @@ parseSomeGuards f = do
885 (e', f) <- 882 (e', f) <-
886 do (e', PCon (_, p) vs) <- try "pattern" $ longPattern <* reservedOp "<-" 883 do (e', PCon (_, p) vs) <- try "pattern" $ longPattern <* reservedOp "<-"
887 checkPattern e' 884 checkPattern e'
888 x <- parseETerm PrecEq 885 x <- parseETerm PrecOp
889 return (e', \gs' gs -> GuardNode x p vs (Alts gs'): gs) 886 return (e', \gs' gs -> GuardNode x p vs (Alts gs'): gs)
890 <|> do x <- parseETerm PrecEq 887 <|> do x <- parseETerm PrecOp
891 return (mempty, \gs' gs -> [GuardNode x "True" [] $ Alts gs', GuardNode x "False" [] $ Alts gs]) 888 return (mempty, \gs' gs -> [GuardNode x "True" [] $ Alts gs', GuardNode x "False" [] $ Alts gs])
892 f <$> ((map (dbfGT e') <$> parseSomeGuards (> pos)) <|> (:[]) . GuardLeaf <$ reservedOp "->" <*> (dbf' e' <$> parseETerm PrecLam)) 889 f <$> ((map (dbfGT e') <$> parseSomeGuards (> pos)) <|> (:[]) . GuardLeaf <$ reservedOp "->" <*> (dbf' e' <$> parseETerm PrecLam))
893 <*> option [] (parseSomeGuards (== pos)) 890 <*> option [] (parseSomeGuards (== pos))
@@ -973,7 +970,7 @@ dbFunAlt v (FunAlt n ts gue) = FunAlt n (map (second $ mapP (dbf' v)) ts) $ fmap
973 970
974mkDesugarInfo :: [Stmt] -> DesugarInfo 971mkDesugarInfo :: [Stmt] -> DesugarInfo
975mkDesugarInfo ss = 972mkDesugarInfo ss =
976 ( Map.fromList [(s, f) | PrecDef (_, s) f <- ss] 973 ( Map.fromList $ ("'EqCTt", (Infix, -1)): [(s, f) | PrecDef (_, s) f <- ss]
977 , Map.fromList $ 974 , Map.fromList $
978 [(cn, Left ((t, pars ty), (snd *** pars) <$> cs)) | Data (_, t) ps ty _ cs <- ss, ((_, cn), ct) <- cs] 975 [(cn, Left ((t, pars ty), (snd *** pars) <$> cs)) | Data (_, t) ps ty _ cs <- ss, ((_, cn), ct) <- cs]
979 ++ [(t, Right $ pars $ addParamsS ps ty) | Data (_, t) ps ty _ cs <- ss] 976 ++ [(t, Right $ pars $ addParamsS ps ty) | Data (_, t) ps ty _ cs <- ss]
diff --git a/testdata/Builtins.out b/testdata/Builtins.out
index 5c4ff581..6f407c39 100644
--- a/testdata/Builtins.out
+++ b/testdata/Builtins.out
@@ -1019,15 +1019,19 @@ testdata/Builtins.lc 329:3-329:10 FragmentOperation (Color V6) | {a} -> {b:Nat}
1019testdata/Builtins.lc 329:3-330:102 Type 1019testdata/Builtins.lc 329:3-330:102 Type
1020testdata/Builtins.lc 329:26-330:102 Type 1020testdata/Builtins.lc 329:26-330:102 Type
1021testdata/Builtins.lc 329:27-329:31 V7 1021testdata/Builtins.lc 329:27-329:31 V7
1022testdata/Builtins.lc 329:27-329:33 Type->Type
1022testdata/Builtins.lc 329:27-329:50 Type 1023testdata/Builtins.lc 329:27-329:50 Type
1024testdata/Builtins.lc 329:32-329:33 Type -> Type->Type
1023testdata/Builtins.lc 329:34-329:43 Nat -> Type->Type 1025testdata/Builtins.lc 329:34-329:43 Nat -> Type->Type
1024testdata/Builtins.lc 329:34-329:45 Type->Type 1026testdata/Builtins.lc 329:34-329:45 Type->Type
1025testdata/Builtins.lc 329:34-329:50 Type 1027testdata/Builtins.lc 329:34-329:50 Type
1026testdata/Builtins.lc 329:44-329:45 V5 1028testdata/Builtins.lc 329:44-329:45 V5
1027testdata/Builtins.lc 329:46-329:50 Type 1029testdata/Builtins.lc 329:46-329:50 Type
1028testdata/Builtins.lc 329:52-329:57 V4 1030testdata/Builtins.lc 329:52-329:57 V4
1031testdata/Builtins.lc 329:52-329:59 Type->Type
1029testdata/Builtins.lc 329:52-329:73 Type 1032testdata/Builtins.lc 329:52-329:73 Type
1030testdata/Builtins.lc 329:52-330:102 Type 1033testdata/Builtins.lc 329:52-330:102 Type
1034testdata/Builtins.lc 329:58-329:59 Type -> Type->Type
1031testdata/Builtins.lc 329:60-329:69 Nat -> Type->Type 1035testdata/Builtins.lc 329:60-329:69 Nat -> Type->Type
1032testdata/Builtins.lc 329:60-329:71 Type->Type 1036testdata/Builtins.lc 329:60-329:71 Type->Type
1033testdata/Builtins.lc 329:60-329:73 Type 1037testdata/Builtins.lc 329:60-329:73 Type
@@ -1219,8 +1223,10 @@ testdata/Builtins.lc 361:42-361:56 Type->Type
1219testdata/Builtins.lc 361:42-361:58 Type 1223testdata/Builtins.lc 361:42-361:58 Type
1220testdata/Builtins.lc 361:57-361:58 V3 1224testdata/Builtins.lc 361:57-361:58 V3
1221testdata/Builtins.lc 361:60-361:61 Type 1225testdata/Builtins.lc 361:60-361:61 Type
1226testdata/Builtins.lc 361:60-361:63 Type->Type
1222testdata/Builtins.lc 361:60-361:74 Type 1227testdata/Builtins.lc 361:60-361:74 Type
1223testdata/Builtins.lc 361:60-361:104 Type 1228testdata/Builtins.lc 361:60-361:104 Type
1229testdata/Builtins.lc 361:62-361:63 Type -> Type->Type
1224testdata/Builtins.lc 361:64-361:71 Type->Type 1230testdata/Builtins.lc 361:64-361:71 Type->Type
1225testdata/Builtins.lc 361:64-361:74 Type 1231testdata/Builtins.lc 361:64-361:74 Type
1226testdata/Builtins.lc 361:72-361:74 V2 1232testdata/Builtins.lc 361:72-361:74 V2
@@ -1367,13 +1373,17 @@ testdata/Builtins.lc 389:47-389:48 V5
1367testdata/Builtins.lc 391:1-391:11 {a} -> {b} -> {c} -> {d:PrimitiveType} -> {e : a ~ InterpolatedType b} -> {f : c ~ JoinTupleType (VecS Float 4) a} -> c->Float -> b -> RasterContext d -> Primitive d c -> Stream (Fragment 1 a) 1373testdata/Builtins.lc 391:1-391:11 {a} -> {b} -> {c} -> {d:PrimitiveType} -> {e : a ~ InterpolatedType b} -> {f : c ~ JoinTupleType (VecS Float 4) a} -> c->Float -> b -> RasterContext d -> Primitive d c -> Stream (Fragment 1 a)
1368testdata/Builtins.lc 391:20-395:55 Type 1374testdata/Builtins.lc 391:20-395:55 Type
1369testdata/Builtins.lc 391:21-391:22 V7 1375testdata/Builtins.lc 391:21-391:22 V7
1376testdata/Builtins.lc 391:21-391:24 Type->Type
1370testdata/Builtins.lc 391:21-391:43 Type 1377testdata/Builtins.lc 391:21-391:43 Type
1378testdata/Builtins.lc 391:23-391:24 Type -> Type->Type
1371testdata/Builtins.lc 391:25-391:41 Type->Type 1379testdata/Builtins.lc 391:25-391:41 Type->Type
1372testdata/Builtins.lc 391:25-391:43 Type 1380testdata/Builtins.lc 391:25-391:43 Type
1373testdata/Builtins.lc 391:42-391:43 V5 1381testdata/Builtins.lc 391:42-391:43 V5
1374testdata/Builtins.lc 391:45-391:46 V4 1382testdata/Builtins.lc 391:45-391:46 V4
1383testdata/Builtins.lc 391:45-391:48 Type->Type
1375testdata/Builtins.lc 391:45-391:78 Type 1384testdata/Builtins.lc 391:45-391:78 Type
1376testdata/Builtins.lc 391:45-395:55 Type 1385testdata/Builtins.lc 391:45-395:55 Type
1386testdata/Builtins.lc 391:47-391:48 Type -> Type->Type
1377testdata/Builtins.lc 391:49-391:62 Type -> Type->Type 1387testdata/Builtins.lc 391:49-391:62 Type -> Type->Type
1378testdata/Builtins.lc 391:49-391:76 Type->Type 1388testdata/Builtins.lc 391:49-391:76 Type->Type
1379testdata/Builtins.lc 391:49-391:78 Type 1389testdata/Builtins.lc 391:49-391:78 Type
@@ -1468,8 +1478,10 @@ testdata/Builtins.lc 409:48-409:51 Type->Type
1468testdata/Builtins.lc 409:48-409:53 Type 1478testdata/Builtins.lc 409:48-409:53 Type
1469testdata/Builtins.lc 409:52-409:53 V3 1479testdata/Builtins.lc 409:52-409:53 V3
1470testdata/Builtins.lc 409:55-409:60 V2 1480testdata/Builtins.lc 409:55-409:60 V2
1481testdata/Builtins.lc 409:55-409:62 Type->Type
1471testdata/Builtins.lc 409:55-409:76 Type 1482testdata/Builtins.lc 409:55-409:76 Type
1472testdata/Builtins.lc 409:55-410:57 Type 1483testdata/Builtins.lc 409:55-410:57 Type
1484testdata/Builtins.lc 409:61-409:62 Type -> Type->Type
1473testdata/Builtins.lc 409:63-409:72 Nat -> Type->Type 1485testdata/Builtins.lc 409:63-409:72 Nat -> Type->Type
1474testdata/Builtins.lc 409:63-409:74 Type->Type 1486testdata/Builtins.lc 409:63-409:74 Type->Type
1475testdata/Builtins.lc 409:63-409:76 Type 1487testdata/Builtins.lc 409:63-409:76 Type
@@ -1644,10 +1656,12 @@ testdata/Builtins.lc 438:56-438:57 V2
1644testdata/Builtins.lc 438:59-438:73 Nat -> Type->Type 1656testdata/Builtins.lc 438:59-438:73 Nat -> Type->Type
1645testdata/Builtins.lc 438:59-438:75 Type->Type 1657testdata/Builtins.lc 438:59-438:75 Type->Type
1646testdata/Builtins.lc 438:59-438:77 Type 1658testdata/Builtins.lc 438:59-438:77 Type
1659testdata/Builtins.lc 438:59-438:79 Type->Type
1647testdata/Builtins.lc 438:59-438:95 Type 1660testdata/Builtins.lc 438:59-438:95 Type
1648testdata/Builtins.lc 438:59-438:120 Type 1661testdata/Builtins.lc 438:59-438:120 Type
1649testdata/Builtins.lc 438:74-438:75 Nat 1662testdata/Builtins.lc 438:74-438:75 Nat
1650testdata/Builtins.lc 438:76-438:77 Type 1663testdata/Builtins.lc 438:76-438:77 Type
1664testdata/Builtins.lc 438:78-438:79 Type -> Type->Type
1651testdata/Builtins.lc 438:80-438:93 Type->Type 1665testdata/Builtins.lc 438:80-438:93 Type->Type
1652testdata/Builtins.lc 438:80-438:95 Type 1666testdata/Builtins.lc 438:80-438:95 Type
1653testdata/Builtins.lc 438:94-438:95 Type 1667testdata/Builtins.lc 438:94-438:95 Type
@@ -1740,7 +1754,9 @@ testdata/Builtins.lc 456:11-456:19 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -
1740testdata/Builtins.lc 456:21-456:29 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b 1754testdata/Builtins.lc 456:21-456:29 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> {d : Num a} -> b -> a->b
1741testdata/Builtins.lc 456:34-456:80 Type 1755testdata/Builtins.lc 456:34-456:80 Type
1742testdata/Builtins.lc 456:35-456:36 V3 1756testdata/Builtins.lc 456:35-456:36 V3
1757testdata/Builtins.lc 456:35-456:38 Type->Type
1743testdata/Builtins.lc 456:35-456:57 Type 1758testdata/Builtins.lc 456:35-456:57 Type
1759testdata/Builtins.lc 456:37-456:38 Type -> Type->Type
1744testdata/Builtins.lc 456:39-456:55 Type->Type 1760testdata/Builtins.lc 456:39-456:55 Type->Type
1745testdata/Builtins.lc 456:39-456:57 Type 1761testdata/Builtins.lc 456:39-456:57 Type
1746testdata/Builtins.lc 456:56-456:57 V1 1762testdata/Builtins.lc 456:56-456:57 V1
@@ -1760,8 +1776,10 @@ testdata/Builtins.lc 457:35-457:38 Type->Type
1760testdata/Builtins.lc 457:35-457:40 Type 1776testdata/Builtins.lc 457:35-457:40 Type
1761testdata/Builtins.lc 457:39-457:40 V5 1777testdata/Builtins.lc 457:39-457:40 V5
1762testdata/Builtins.lc 457:42-457:43 V4 1778testdata/Builtins.lc 457:42-457:43 V4
1779testdata/Builtins.lc 457:42-457:45 Type->Type
1763testdata/Builtins.lc 457:42-457:59 Type 1780testdata/Builtins.lc 457:42-457:59 Type
1764testdata/Builtins.lc 457:42-457:75 Type 1781testdata/Builtins.lc 457:42-457:75 Type
1782testdata/Builtins.lc 457:44-457:45 Type -> Type->Type
1765testdata/Builtins.lc 457:46-457:55 Nat -> Type->Type 1783testdata/Builtins.lc 457:46-457:55 Nat -> Type->Type
1766testdata/Builtins.lc 457:46-457:57 Type->Type 1784testdata/Builtins.lc 457:46-457:57 Type->Type
1767testdata/Builtins.lc 457:46-457:59 Type 1785testdata/Builtins.lc 457:46-457:59 Type
@@ -1779,8 +1797,10 @@ testdata/Builtins.lc 458:35-458:38 Type->Type
1779testdata/Builtins.lc 458:35-458:40 Type 1797testdata/Builtins.lc 458:35-458:40 Type
1780testdata/Builtins.lc 458:39-458:40 V5 1798testdata/Builtins.lc 458:39-458:40 V5
1781testdata/Builtins.lc 458:42-458:43 V4 1799testdata/Builtins.lc 458:42-458:43 V4
1800testdata/Builtins.lc 458:42-458:45 Type->Type
1782testdata/Builtins.lc 458:42-458:59 Type 1801testdata/Builtins.lc 458:42-458:59 Type
1783testdata/Builtins.lc 458:42-458:75 Type 1802testdata/Builtins.lc 458:42-458:75 Type
1803testdata/Builtins.lc 458:44-458:45 Type -> Type->Type
1784testdata/Builtins.lc 458:46-458:55 Nat -> Type->Type 1804testdata/Builtins.lc 458:46-458:55 Nat -> Type->Type
1785testdata/Builtins.lc 458:46-458:57 Type->Type 1805testdata/Builtins.lc 458:46-458:57 Type->Type
1786testdata/Builtins.lc 458:46-458:59 Type 1806testdata/Builtins.lc 458:46-458:59 Type
@@ -1809,8 +1829,10 @@ testdata/Builtins.lc 461:35-461:43 Type->Type
1809testdata/Builtins.lc 461:35-461:45 Type 1829testdata/Builtins.lc 461:35-461:45 Type
1810testdata/Builtins.lc 461:44-461:45 V5 1830testdata/Builtins.lc 461:44-461:45 V5
1811testdata/Builtins.lc 461:47-461:48 V4 1831testdata/Builtins.lc 461:47-461:48 V4
1832testdata/Builtins.lc 461:47-461:50 Type->Type
1812testdata/Builtins.lc 461:47-461:64 Type 1833testdata/Builtins.lc 461:47-461:64 Type
1813testdata/Builtins.lc 461:47-461:80 Type 1834testdata/Builtins.lc 461:47-461:80 Type
1835testdata/Builtins.lc 461:49-461:50 Type -> Type->Type
1814testdata/Builtins.lc 461:51-461:60 Nat -> Type->Type 1836testdata/Builtins.lc 461:51-461:60 Nat -> Type->Type
1815testdata/Builtins.lc 461:51-461:62 Type->Type 1837testdata/Builtins.lc 461:51-461:62 Type->Type
1816testdata/Builtins.lc 461:51-461:64 Type 1838testdata/Builtins.lc 461:51-461:64 Type
@@ -1829,8 +1851,10 @@ testdata/Builtins.lc 462:35-462:43 Type->Type
1829testdata/Builtins.lc 462:35-462:45 Type 1851testdata/Builtins.lc 462:35-462:45 Type
1830testdata/Builtins.lc 462:44-462:45 V5 1852testdata/Builtins.lc 462:44-462:45 V5
1831testdata/Builtins.lc 462:47-462:48 V4 1853testdata/Builtins.lc 462:47-462:48 V4
1854testdata/Builtins.lc 462:47-462:50 Type->Type
1832testdata/Builtins.lc 462:47-462:64 Type 1855testdata/Builtins.lc 462:47-462:64 Type
1833testdata/Builtins.lc 462:47-462:80 Type 1856testdata/Builtins.lc 462:47-462:80 Type
1857testdata/Builtins.lc 462:49-462:50 Type -> Type->Type
1834testdata/Builtins.lc 462:51-462:60 Nat -> Type->Type 1858testdata/Builtins.lc 462:51-462:60 Nat -> Type->Type
1835testdata/Builtins.lc 462:51-462:62 Type->Type 1859testdata/Builtins.lc 462:51-462:62 Type->Type
1836testdata/Builtins.lc 462:51-462:64 Type 1860testdata/Builtins.lc 462:51-462:64 Type
@@ -1847,8 +1871,10 @@ testdata/Builtins.lc 463:35-463:43 Type->Type
1847testdata/Builtins.lc 463:35-463:45 Type 1871testdata/Builtins.lc 463:35-463:45 Type
1848testdata/Builtins.lc 463:44-463:45 V5 1872testdata/Builtins.lc 463:44-463:45 V5
1849testdata/Builtins.lc 463:47-463:48 V4 1873testdata/Builtins.lc 463:47-463:48 V4
1874testdata/Builtins.lc 463:47-463:50 Type->Type
1850testdata/Builtins.lc 463:47-463:64 Type 1875testdata/Builtins.lc 463:47-463:64 Type
1851testdata/Builtins.lc 463:47-463:75 Type 1876testdata/Builtins.lc 463:47-463:75 Type
1877testdata/Builtins.lc 463:49-463:50 Type -> Type->Type
1852testdata/Builtins.lc 463:51-463:60 Nat -> Type->Type 1878testdata/Builtins.lc 463:51-463:60 Nat -> Type->Type
1853testdata/Builtins.lc 463:51-463:62 Type->Type 1879testdata/Builtins.lc 463:51-463:62 Type->Type
1854testdata/Builtins.lc 463:51-463:64 Type 1880testdata/Builtins.lc 463:51-463:64 Type
@@ -1864,16 +1890,20 @@ testdata/Builtins.lc 464:35-464:43 Type->Type
1864testdata/Builtins.lc 464:35-464:45 Type 1890testdata/Builtins.lc 464:35-464:45 Type
1865testdata/Builtins.lc 464:44-464:45 V7 1891testdata/Builtins.lc 464:44-464:45 V7
1866testdata/Builtins.lc 464:47-464:48 V6 1892testdata/Builtins.lc 464:47-464:48 V6
1893testdata/Builtins.lc 464:47-464:50 Type->Type
1867testdata/Builtins.lc 464:47-464:64 Type 1894testdata/Builtins.lc 464:47-464:64 Type
1868testdata/Builtins.lc 464:47-464:102 Type 1895testdata/Builtins.lc 464:47-464:102 Type
1896testdata/Builtins.lc 464:49-464:50 Type -> Type->Type
1869testdata/Builtins.lc 464:51-464:60 Nat -> Type->Type 1897testdata/Builtins.lc 464:51-464:60 Nat -> Type->Type
1870testdata/Builtins.lc 464:51-464:62 Type->Type 1898testdata/Builtins.lc 464:51-464:62 Type->Type
1871testdata/Builtins.lc 464:51-464:64 Type 1899testdata/Builtins.lc 464:51-464:64 Type
1872testdata/Builtins.lc 464:61-464:62 V4 1900testdata/Builtins.lc 464:61-464:62 V4
1873testdata/Builtins.lc 464:63-464:64 Type 1901testdata/Builtins.lc 464:63-464:64 Type
1874testdata/Builtins.lc 464:66-464:67 V3 1902testdata/Builtins.lc 464:66-464:67 V3
1903testdata/Builtins.lc 464:66-464:69 Type->Type
1875testdata/Builtins.lc 464:66-464:86 Type 1904testdata/Builtins.lc 464:66-464:86 Type
1876testdata/Builtins.lc 464:66-464:102 Type 1905testdata/Builtins.lc 464:66-464:102 Type
1906testdata/Builtins.lc 464:68-464:69 Type -> Type->Type
1877testdata/Builtins.lc 464:70-464:79 Nat -> Type->Type 1907testdata/Builtins.lc 464:70-464:79 Nat -> Type->Type
1878testdata/Builtins.lc 464:70-464:81 Type->Type 1908testdata/Builtins.lc 464:70-464:81 Type->Type
1879testdata/Builtins.lc 464:70-464:86 Type 1909testdata/Builtins.lc 464:70-464:86 Type
@@ -1891,8 +1921,10 @@ testdata/Builtins.lc 465:35-465:43 Type->Type
1891testdata/Builtins.lc 465:35-465:45 Type 1921testdata/Builtins.lc 465:35-465:45 Type
1892testdata/Builtins.lc 465:44-465:45 V5 1922testdata/Builtins.lc 465:44-465:45 V5
1893testdata/Builtins.lc 465:47-465:48 V4 1923testdata/Builtins.lc 465:47-465:48 V4
1924testdata/Builtins.lc 465:47-465:50 Type->Type
1894testdata/Builtins.lc 465:47-465:64 Type 1925testdata/Builtins.lc 465:47-465:64 Type
1895testdata/Builtins.lc 465:47-465:83 Type 1926testdata/Builtins.lc 465:47-465:83 Type
1927testdata/Builtins.lc 465:49-465:50 Type -> Type->Type
1896testdata/Builtins.lc 465:51-465:60 Nat -> Type->Type 1928testdata/Builtins.lc 465:51-465:60 Nat -> Type->Type
1897testdata/Builtins.lc 465:51-465:62 Type->Type 1929testdata/Builtins.lc 465:51-465:62 Type->Type
1898testdata/Builtins.lc 465:51-465:64 Type 1930testdata/Builtins.lc 465:51-465:64 Type
@@ -1914,6 +1946,8 @@ testdata/Builtins.lc 468:1-468:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Bool} -
1914testdata/Builtins.lc 468:34-468:56 Type 1946testdata/Builtins.lc 468:34-468:56 Type
1915testdata/Builtins.lc 468:34-468:66 Type 1947testdata/Builtins.lc 468:34-468:66 Type
1916testdata/Builtins.lc 468:35-468:36 V3 1948testdata/Builtins.lc 468:35-468:36 V3
1949testdata/Builtins.lc 468:35-468:38 Type->Type
1950testdata/Builtins.lc 468:37-468:38 Type -> Type->Type
1917testdata/Builtins.lc 468:39-468:48 Nat -> Type->Type 1951testdata/Builtins.lc 468:39-468:48 Nat -> Type->Type
1918testdata/Builtins.lc 468:39-468:50 Type->Type 1952testdata/Builtins.lc 468:39-468:50 Type->Type
1919testdata/Builtins.lc 468:39-468:55 Type 1953testdata/Builtins.lc 468:39-468:55 Type
@@ -1954,6 +1988,8 @@ testdata/Builtins.lc 472:195-472:206 {a} -> {b:Nat} -> {c : a ~ VecScalar b Flo
1954testdata/Builtins.lc 473:34-473:57 Type 1988testdata/Builtins.lc 473:34-473:57 Type
1955testdata/Builtins.lc 473:34-473:67 Type 1989testdata/Builtins.lc 473:34-473:67 Type
1956testdata/Builtins.lc 473:35-473:36 V3 1990testdata/Builtins.lc 473:35-473:36 V3
1991testdata/Builtins.lc 473:35-473:38 Type->Type
1992testdata/Builtins.lc 473:37-473:38 Type -> Type->Type
1957testdata/Builtins.lc 473:39-473:48 Nat -> Type->Type 1993testdata/Builtins.lc 473:39-473:48 Nat -> Type->Type
1958testdata/Builtins.lc 473:39-473:50 Type->Type 1994testdata/Builtins.lc 473:39-473:50 Type->Type
1959testdata/Builtins.lc 473:39-473:56 Type 1995testdata/Builtins.lc 473:39-473:56 Type
@@ -1967,6 +2003,8 @@ testdata/Builtins.lc 474:10-474:19 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float
1967testdata/Builtins.lc 474:34-474:57 Type 2003testdata/Builtins.lc 474:34-474:57 Type
1968testdata/Builtins.lc 474:34-474:72 Type 2004testdata/Builtins.lc 474:34-474:72 Type
1969testdata/Builtins.lc 474:35-474:36 V3 2005testdata/Builtins.lc 474:35-474:36 V3
2006testdata/Builtins.lc 474:35-474:38 Type->Type
2007testdata/Builtins.lc 474:37-474:38 Type -> Type->Type
1970testdata/Builtins.lc 474:39-474:48 Nat -> Type->Type 2008testdata/Builtins.lc 474:39-474:48 Nat -> Type->Type
1971testdata/Builtins.lc 474:39-474:50 Type->Type 2009testdata/Builtins.lc 474:39-474:50 Type->Type
1972testdata/Builtins.lc 474:39-474:56 Type 2010testdata/Builtins.lc 474:39-474:56 Type
@@ -1986,6 +2024,8 @@ testdata/Builtins.lc 476:59-476:68 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float
1986testdata/Builtins.lc 477:34-477:57 Type 2024testdata/Builtins.lc 477:34-477:57 Type
1987testdata/Builtins.lc 477:34-477:67 Type 2025testdata/Builtins.lc 477:34-477:67 Type
1988testdata/Builtins.lc 477:35-477:36 V3 2026testdata/Builtins.lc 477:35-477:36 V3
2027testdata/Builtins.lc 477:35-477:38 Type->Type
2028testdata/Builtins.lc 477:37-477:38 Type -> Type->Type
1989testdata/Builtins.lc 477:39-477:48 Nat -> Type->Type 2029testdata/Builtins.lc 477:39-477:48 Nat -> Type->Type
1990testdata/Builtins.lc 477:39-477:50 Type->Type 2030testdata/Builtins.lc 477:39-477:50 Type->Type
1991testdata/Builtins.lc 477:39-477:56 Type 2031testdata/Builtins.lc 477:39-477:56 Type
@@ -2001,8 +2041,10 @@ testdata/Builtins.lc 478:35-478:38 Type->Type
2001testdata/Builtins.lc 478:35-478:40 Type 2041testdata/Builtins.lc 478:35-478:40 Type
2002testdata/Builtins.lc 478:39-478:40 V5 2042testdata/Builtins.lc 478:39-478:40 V5
2003testdata/Builtins.lc 478:42-478:43 V4 2043testdata/Builtins.lc 478:42-478:43 V4
2044testdata/Builtins.lc 478:42-478:45 Type->Type
2004testdata/Builtins.lc 478:42-478:59 Type 2045testdata/Builtins.lc 478:42-478:59 Type
2005testdata/Builtins.lc 478:42-478:75 Type 2046testdata/Builtins.lc 478:42-478:75 Type
2047testdata/Builtins.lc 478:44-478:45 Type -> Type->Type
2006testdata/Builtins.lc 478:46-478:55 Nat -> Type->Type 2048testdata/Builtins.lc 478:46-478:55 Nat -> Type->Type
2007testdata/Builtins.lc 478:46-478:57 Type->Type 2049testdata/Builtins.lc 478:46-478:57 Type->Type
2008testdata/Builtins.lc 478:46-478:59 Type 2050testdata/Builtins.lc 478:46-478:59 Type
@@ -2020,8 +2062,10 @@ testdata/Builtins.lc 479:35-479:38 Type->Type
2020testdata/Builtins.lc 479:35-479:40 Type 2062testdata/Builtins.lc 479:35-479:40 Type
2021testdata/Builtins.lc 479:39-479:40 V5 2063testdata/Builtins.lc 479:39-479:40 V5
2022testdata/Builtins.lc 479:42-479:43 V4 2064testdata/Builtins.lc 479:42-479:43 V4
2065testdata/Builtins.lc 479:42-479:45 Type->Type
2023testdata/Builtins.lc 479:42-479:59 Type 2066testdata/Builtins.lc 479:42-479:59 Type
2024testdata/Builtins.lc 479:42-479:75 Type 2067testdata/Builtins.lc 479:42-479:75 Type
2068testdata/Builtins.lc 479:44-479:45 Type -> Type->Type
2025testdata/Builtins.lc 479:46-479:55 Nat -> Type->Type 2069testdata/Builtins.lc 479:46-479:55 Nat -> Type->Type
2026testdata/Builtins.lc 479:46-479:57 Type->Type 2070testdata/Builtins.lc 479:46-479:57 Type->Type
2027testdata/Builtins.lc 479:46-479:59 Type 2071testdata/Builtins.lc 479:46-479:59 Type
@@ -2036,15 +2080,19 @@ testdata/Builtins.lc 480:1-480:10 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b
2036testdata/Builtins.lc 480:12-480:21 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c 2080testdata/Builtins.lc 480:12-480:21 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a->c
2037testdata/Builtins.lc 480:34-480:89 Type 2081testdata/Builtins.lc 480:34-480:89 Type
2038testdata/Builtins.lc 480:35-480:36 V5 2082testdata/Builtins.lc 480:35-480:36 V5
2083testdata/Builtins.lc 480:35-480:38 Type->Type
2039testdata/Builtins.lc 480:35-480:56 Type 2084testdata/Builtins.lc 480:35-480:56 Type
2085testdata/Builtins.lc 480:37-480:38 Type -> Type->Type
2040testdata/Builtins.lc 480:39-480:48 Nat -> Type->Type 2086testdata/Builtins.lc 480:39-480:48 Nat -> Type->Type
2041testdata/Builtins.lc 480:39-480:50 Type->Type 2087testdata/Builtins.lc 480:39-480:50 Type->Type
2042testdata/Builtins.lc 480:39-480:56 Type 2088testdata/Builtins.lc 480:39-480:56 Type
2043testdata/Builtins.lc 480:49-480:50 V3 2089testdata/Builtins.lc 480:49-480:50 V3
2044testdata/Builtins.lc 480:51-480:56 Type 2090testdata/Builtins.lc 480:51-480:56 Type
2045testdata/Builtins.lc 480:58-480:59 V2 2091testdata/Builtins.lc 480:58-480:59 V2
2092testdata/Builtins.lc 480:58-480:61 Type->Type
2046testdata/Builtins.lc 480:58-480:78 Type 2093testdata/Builtins.lc 480:58-480:78 Type
2047testdata/Builtins.lc 480:58-480:89 Type 2094testdata/Builtins.lc 480:58-480:89 Type
2095testdata/Builtins.lc 480:60-480:61 Type -> Type->Type
2048testdata/Builtins.lc 480:62-480:71 Nat -> Type->Type 2096testdata/Builtins.lc 480:62-480:71 Nat -> Type->Type
2049testdata/Builtins.lc 480:62-480:73 Type->Type 2097testdata/Builtins.lc 480:62-480:73 Type->Type
2050testdata/Builtins.lc 480:62-480:78 Type 2098testdata/Builtins.lc 480:62-480:78 Type
@@ -2060,8 +2108,10 @@ testdata/Builtins.lc 481:35-481:41 Type->Type
2060testdata/Builtins.lc 481:35-481:43 Type 2108testdata/Builtins.lc 481:35-481:43 Type
2061testdata/Builtins.lc 481:42-481:43 V5 2109testdata/Builtins.lc 481:42-481:43 V5
2062testdata/Builtins.lc 481:45-481:46 V4 2110testdata/Builtins.lc 481:45-481:46 V4
2111testdata/Builtins.lc 481:45-481:48 Type->Type
2063testdata/Builtins.lc 481:45-481:62 Type 2112testdata/Builtins.lc 481:45-481:62 Type
2064testdata/Builtins.lc 481:45-481:73 Type 2113testdata/Builtins.lc 481:45-481:73 Type
2114testdata/Builtins.lc 481:47-481:48 Type -> Type->Type
2065testdata/Builtins.lc 481:49-481:58 Nat -> Type->Type 2115testdata/Builtins.lc 481:49-481:58 Nat -> Type->Type
2066testdata/Builtins.lc 481:49-481:60 Type->Type 2116testdata/Builtins.lc 481:49-481:60 Type->Type
2067testdata/Builtins.lc 481:49-481:62 Type 2117testdata/Builtins.lc 481:49-481:62 Type
@@ -2074,6 +2124,8 @@ testdata/Builtins.lc 482:1-482:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float}
2074testdata/Builtins.lc 482:34-482:57 Type 2124testdata/Builtins.lc 482:34-482:57 Type
2075testdata/Builtins.lc 482:34-482:72 Type 2125testdata/Builtins.lc 482:34-482:72 Type
2076testdata/Builtins.lc 482:35-482:36 V3 2126testdata/Builtins.lc 482:35-482:36 V3
2127testdata/Builtins.lc 482:35-482:38 Type->Type
2128testdata/Builtins.lc 482:37-482:38 Type -> Type->Type
2077testdata/Builtins.lc 482:39-482:48 Nat -> Type->Type 2129testdata/Builtins.lc 482:39-482:48 Nat -> Type->Type
2078testdata/Builtins.lc 482:39-482:50 Type->Type 2130testdata/Builtins.lc 482:39-482:50 Type->Type
2079testdata/Builtins.lc 482:39-482:56 Type 2131testdata/Builtins.lc 482:39-482:56 Type
@@ -2090,8 +2142,10 @@ testdata/Builtins.lc 483:35-483:38 Type->Type
2090testdata/Builtins.lc 483:35-483:40 Type 2142testdata/Builtins.lc 483:35-483:40 Type
2091testdata/Builtins.lc 483:39-483:40 V5 2143testdata/Builtins.lc 483:39-483:40 V5
2092testdata/Builtins.lc 483:42-483:43 V4 2144testdata/Builtins.lc 483:42-483:43 V4
2145testdata/Builtins.lc 483:42-483:45 Type->Type
2093testdata/Builtins.lc 483:42-483:59 Type 2146testdata/Builtins.lc 483:42-483:59 Type
2094testdata/Builtins.lc 483:42-483:80 Type 2147testdata/Builtins.lc 483:42-483:80 Type
2148testdata/Builtins.lc 483:44-483:45 Type -> Type->Type
2095testdata/Builtins.lc 483:46-483:55 Nat -> Type->Type 2149testdata/Builtins.lc 483:46-483:55 Nat -> Type->Type
2096testdata/Builtins.lc 483:46-483:57 Type->Type 2150testdata/Builtins.lc 483:46-483:57 Type->Type
2097testdata/Builtins.lc 483:46-483:59 Type 2151testdata/Builtins.lc 483:46-483:59 Type
@@ -2110,8 +2164,10 @@ testdata/Builtins.lc 484:35-484:38 Type->Type
2110testdata/Builtins.lc 484:35-484:40 Type 2164testdata/Builtins.lc 484:35-484:40 Type
2111testdata/Builtins.lc 484:39-484:40 V5 2165testdata/Builtins.lc 484:39-484:40 V5
2112testdata/Builtins.lc 484:42-484:43 V4 2166testdata/Builtins.lc 484:42-484:43 V4
2167testdata/Builtins.lc 484:42-484:45 Type->Type
2113testdata/Builtins.lc 484:42-484:59 Type 2168testdata/Builtins.lc 484:42-484:59 Type
2114testdata/Builtins.lc 484:42-484:80 Type 2169testdata/Builtins.lc 484:42-484:80 Type
2170testdata/Builtins.lc 484:44-484:45 Type -> Type->Type
2115testdata/Builtins.lc 484:46-484:55 Nat -> Type->Type 2171testdata/Builtins.lc 484:46-484:55 Nat -> Type->Type
2116testdata/Builtins.lc 484:46-484:57 Type->Type 2172testdata/Builtins.lc 484:46-484:57 Type->Type
2117testdata/Builtins.lc 484:46-484:59 Type 2173testdata/Builtins.lc 484:46-484:59 Type
@@ -2128,6 +2184,8 @@ testdata/Builtins.lc 485:1-485:8 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float}
2128testdata/Builtins.lc 485:34-485:57 Type 2184testdata/Builtins.lc 485:34-485:57 Type
2129testdata/Builtins.lc 485:34-485:77 Type 2185testdata/Builtins.lc 485:34-485:77 Type
2130testdata/Builtins.lc 485:35-485:36 V3 2186testdata/Builtins.lc 485:35-485:36 V3
2187testdata/Builtins.lc 485:35-485:38 Type->Type
2188testdata/Builtins.lc 485:37-485:38 Type -> Type->Type
2131testdata/Builtins.lc 485:39-485:48 Nat -> Type->Type 2189testdata/Builtins.lc 485:39-485:48 Nat -> Type->Type
2132testdata/Builtins.lc 485:39-485:50 Type->Type 2190testdata/Builtins.lc 485:39-485:50 Type->Type
2133testdata/Builtins.lc 485:39-485:56 Type 2191testdata/Builtins.lc 485:39-485:56 Type
@@ -2144,6 +2202,8 @@ testdata/Builtins.lc 486:1-486:9 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float}
2144testdata/Builtins.lc 486:34-486:57 Type 2202testdata/Builtins.lc 486:34-486:57 Type
2145testdata/Builtins.lc 486:34-486:81 Type 2203testdata/Builtins.lc 486:34-486:81 Type
2146testdata/Builtins.lc 486:35-486:36 V3 2204testdata/Builtins.lc 486:35-486:36 V3
2205testdata/Builtins.lc 486:35-486:38 Type->Type
2206testdata/Builtins.lc 486:37-486:38 Type -> Type->Type
2147testdata/Builtins.lc 486:39-486:48 Nat -> Type->Type 2207testdata/Builtins.lc 486:39-486:48 Nat -> Type->Type
2148testdata/Builtins.lc 486:39-486:50 Type->Type 2208testdata/Builtins.lc 486:39-486:50 Type->Type
2149testdata/Builtins.lc 486:39-486:56 Type 2209testdata/Builtins.lc 486:39-486:56 Type
@@ -2159,15 +2219,19 @@ testdata/Builtins.lc 486:80-486:81 Type
2159testdata/Builtins.lc 487:1-487:9 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a -> a -> c->a 2219testdata/Builtins.lc 487:1-487:9 {a} -> {b:Nat} -> {c} -> {d : a ~ VecScalar b Float} -> {e : c ~ VecScalar b Bool} -> a -> a -> c->a
2160testdata/Builtins.lc 487:34-487:99 Type 2220testdata/Builtins.lc 487:34-487:99 Type
2161testdata/Builtins.lc 487:35-487:36 V5 2221testdata/Builtins.lc 487:35-487:36 V5
2222testdata/Builtins.lc 487:35-487:38 Type->Type
2162testdata/Builtins.lc 487:35-487:56 Type 2223testdata/Builtins.lc 487:35-487:56 Type
2224testdata/Builtins.lc 487:37-487:38 Type -> Type->Type
2163testdata/Builtins.lc 487:39-487:48 Nat -> Type->Type 2225testdata/Builtins.lc 487:39-487:48 Nat -> Type->Type
2164testdata/Builtins.lc 487:39-487:50 Type->Type 2226testdata/Builtins.lc 487:39-487:50 Type->Type
2165testdata/Builtins.lc 487:39-487:56 Type 2227testdata/Builtins.lc 487:39-487:56 Type
2166testdata/Builtins.lc 487:49-487:50 V3 2228testdata/Builtins.lc 487:49-487:50 V3
2167testdata/Builtins.lc 487:51-487:56 Type 2229testdata/Builtins.lc 487:51-487:56 Type
2168testdata/Builtins.lc 487:58-487:59 V2 2230testdata/Builtins.lc 487:58-487:59 V2
2231testdata/Builtins.lc 487:58-487:61 Type->Type
2169testdata/Builtins.lc 487:58-487:78 Type 2232testdata/Builtins.lc 487:58-487:78 Type
2170testdata/Builtins.lc 487:58-487:99 Type 2233testdata/Builtins.lc 487:58-487:99 Type
2234testdata/Builtins.lc 487:60-487:61 Type -> Type->Type
2171testdata/Builtins.lc 487:62-487:71 Nat -> Type->Type 2235testdata/Builtins.lc 487:62-487:71 Nat -> Type->Type
2172testdata/Builtins.lc 487:62-487:73 Type->Type 2236testdata/Builtins.lc 487:62-487:73 Type->Type
2173testdata/Builtins.lc 487:62-487:78 Type 2237testdata/Builtins.lc 487:62-487:78 Type
@@ -2184,6 +2248,8 @@ testdata/Builtins.lc 488:1-488:9 {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a
2184testdata/Builtins.lc 488:34-488:53 Type 2248testdata/Builtins.lc 488:34-488:53 Type
2185testdata/Builtins.lc 488:34-488:68 Type 2249testdata/Builtins.lc 488:34-488:68 Type
2186testdata/Builtins.lc 488:35-488:36 V3 2250testdata/Builtins.lc 488:35-488:36 V3
2251testdata/Builtins.lc 488:35-488:38 Type->Type
2252testdata/Builtins.lc 488:37-488:38 Type -> Type->Type
2187testdata/Builtins.lc 488:39-488:44 Nat -> Type->Type 2253testdata/Builtins.lc 488:39-488:44 Nat -> Type->Type
2188testdata/Builtins.lc 488:39-488:46 Type->Type 2254testdata/Builtins.lc 488:39-488:46 Type->Type
2189testdata/Builtins.lc 488:39-488:52 Type 2255testdata/Builtins.lc 488:39-488:52 Type
@@ -2198,6 +2264,8 @@ testdata/Builtins.lc 489:1-489:10 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float}
2198testdata/Builtins.lc 489:34-489:57 Type 2264testdata/Builtins.lc 489:34-489:57 Type
2199testdata/Builtins.lc 489:34-489:76 Type 2265testdata/Builtins.lc 489:34-489:76 Type
2200testdata/Builtins.lc 489:35-489:36 V3 2266testdata/Builtins.lc 489:35-489:36 V3
2267testdata/Builtins.lc 489:35-489:38 Type->Type
2268testdata/Builtins.lc 489:37-489:38 Type -> Type->Type
2201testdata/Builtins.lc 489:39-489:48 Nat -> Type->Type 2269testdata/Builtins.lc 489:39-489:48 Nat -> Type->Type
2202testdata/Builtins.lc 489:39-489:50 Type->Type 2270testdata/Builtins.lc 489:39-489:50 Type->Type
2203testdata/Builtins.lc 489:39-489:56 Type 2271testdata/Builtins.lc 489:39-489:56 Type
@@ -2212,6 +2280,8 @@ testdata/Builtins.lc 490:1-490:15 {a} -> {b:Nat} -> {c : a ~ VecS Float b} -> a
2212testdata/Builtins.lc 490:34-490:53 Type 2280testdata/Builtins.lc 490:34-490:53 Type
2213testdata/Builtins.lc 490:34-490:73 Type 2281testdata/Builtins.lc 490:34-490:73 Type
2214testdata/Builtins.lc 490:35-490:36 V3 2282testdata/Builtins.lc 490:35-490:36 V3
2283testdata/Builtins.lc 490:35-490:38 Type->Type
2284testdata/Builtins.lc 490:37-490:38 Type -> Type->Type
2215testdata/Builtins.lc 490:39-490:44 Nat -> Type->Type 2285testdata/Builtins.lc 490:39-490:44 Nat -> Type->Type
2216testdata/Builtins.lc 490:39-490:46 Type->Type 2286testdata/Builtins.lc 490:39-490:46 Type->Type
2217testdata/Builtins.lc 490:39-490:52 Type 2287testdata/Builtins.lc 490:39-490:52 Type
@@ -2228,6 +2298,8 @@ testdata/Builtins.lc 491:1-491:16 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float}
2228testdata/Builtins.lc 491:34-491:57 Type 2298testdata/Builtins.lc 491:34-491:57 Type
2229testdata/Builtins.lc 491:34-491:85 Type 2299testdata/Builtins.lc 491:34-491:85 Type
2230testdata/Builtins.lc 491:35-491:36 V3 2300testdata/Builtins.lc 491:35-491:36 V3
2301testdata/Builtins.lc 491:35-491:38 Type->Type
2302testdata/Builtins.lc 491:37-491:38 Type -> Type->Type
2231testdata/Builtins.lc 491:39-491:48 Nat -> Type->Type 2303testdata/Builtins.lc 491:39-491:48 Nat -> Type->Type
2232testdata/Builtins.lc 491:39-491:50 Type->Type 2304testdata/Builtins.lc 491:39-491:50 Type->Type
2233testdata/Builtins.lc 491:39-491:56 Type 2305testdata/Builtins.lc 491:39-491:56 Type
@@ -2292,6 +2364,8 @@ testdata/Builtins.lc 499:1-499:11 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float}
2292testdata/Builtins.lc 499:34-499:57 Type 2364testdata/Builtins.lc 499:34-499:57 Type
2293testdata/Builtins.lc 499:34-499:71 Type 2365testdata/Builtins.lc 499:34-499:71 Type
2294testdata/Builtins.lc 499:35-499:36 V3 2366testdata/Builtins.lc 499:35-499:36 V3
2367testdata/Builtins.lc 499:35-499:38 Type->Type
2368testdata/Builtins.lc 499:37-499:38 Type -> Type->Type
2295testdata/Builtins.lc 499:39-499:48 Nat -> Type->Type 2369testdata/Builtins.lc 499:39-499:48 Nat -> Type->Type
2296testdata/Builtins.lc 499:39-499:50 Type->Type 2370testdata/Builtins.lc 499:39-499:50 Type->Type
2297testdata/Builtins.lc 499:39-499:56 Type 2371testdata/Builtins.lc 499:39-499:56 Type
@@ -2305,6 +2379,8 @@ testdata/Builtins.lc 500:15-500:22 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float
2305testdata/Builtins.lc 500:34-500:57 Type 2379testdata/Builtins.lc 500:34-500:57 Type
2306testdata/Builtins.lc 500:34-500:76 Type 2380testdata/Builtins.lc 500:34-500:76 Type
2307testdata/Builtins.lc 500:35-500:36 V3 2381testdata/Builtins.lc 500:35-500:36 V3
2382testdata/Builtins.lc 500:35-500:38 Type->Type
2383testdata/Builtins.lc 500:37-500:38 Type -> Type->Type
2308testdata/Builtins.lc 500:39-500:48 Nat -> Type->Type 2384testdata/Builtins.lc 500:39-500:48 Nat -> Type->Type
2309testdata/Builtins.lc 500:39-500:50 Type->Type 2385testdata/Builtins.lc 500:39-500:50 Type->Type
2310testdata/Builtins.lc 500:39-500:56 Type 2386testdata/Builtins.lc 500:39-500:56 Type
@@ -2319,6 +2395,8 @@ testdata/Builtins.lc 501:1-501:10 {a} -> {b : a ~ VecS Float 3} -> a -> a->a
2319testdata/Builtins.lc 501:34-501:57 Type 2395testdata/Builtins.lc 501:34-501:57 Type
2320testdata/Builtins.lc 501:34-501:72 Type 2396testdata/Builtins.lc 501:34-501:72 Type
2321testdata/Builtins.lc 501:35-501:36 V1 2397testdata/Builtins.lc 501:35-501:36 V1
2398testdata/Builtins.lc 501:35-501:38 Type->Type
2399testdata/Builtins.lc 501:37-501:38 Type -> Type->Type
2322testdata/Builtins.lc 501:39-501:48 Nat -> Type->Type 2400testdata/Builtins.lc 501:39-501:48 Nat -> Type->Type
2323testdata/Builtins.lc 501:39-501:50 Type->Type 2401testdata/Builtins.lc 501:39-501:50 Type->Type
2324testdata/Builtins.lc 501:39-501:56 Type 2402testdata/Builtins.lc 501:39-501:56 Type
@@ -2333,6 +2411,8 @@ testdata/Builtins.lc 502:1-502:14 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float}
2333testdata/Builtins.lc 502:34-502:57 Type 2411testdata/Builtins.lc 502:34-502:57 Type
2334testdata/Builtins.lc 502:34-502:67 Type 2412testdata/Builtins.lc 502:34-502:67 Type
2335testdata/Builtins.lc 502:35-502:36 V3 2413testdata/Builtins.lc 502:35-502:36 V3
2414testdata/Builtins.lc 502:35-502:38 Type->Type
2415testdata/Builtins.lc 502:37-502:38 Type -> Type->Type
2336testdata/Builtins.lc 502:39-502:48 Nat -> Type->Type 2416testdata/Builtins.lc 502:39-502:48 Nat -> Type->Type
2337testdata/Builtins.lc 502:39-502:50 Type->Type 2417testdata/Builtins.lc 502:39-502:50 Type->Type
2338testdata/Builtins.lc 502:39-502:56 Type 2418testdata/Builtins.lc 502:39-502:56 Type
@@ -2346,6 +2426,8 @@ testdata/Builtins.lc 503:18-503:29 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float
2346testdata/Builtins.lc 503:34-503:57 Type 2426testdata/Builtins.lc 503:34-503:57 Type
2347testdata/Builtins.lc 503:34-503:77 Type 2427testdata/Builtins.lc 503:34-503:77 Type
2348testdata/Builtins.lc 503:35-503:36 V3 2428testdata/Builtins.lc 503:35-503:36 V3
2429testdata/Builtins.lc 503:35-503:38 Type->Type
2430testdata/Builtins.lc 503:37-503:38 Type -> Type->Type
2349testdata/Builtins.lc 503:39-503:48 Nat -> Type->Type 2431testdata/Builtins.lc 503:39-503:48 Nat -> Type->Type
2350testdata/Builtins.lc 503:39-503:50 Type->Type 2432testdata/Builtins.lc 503:39-503:50 Type->Type
2351testdata/Builtins.lc 503:39-503:56 Type 2433testdata/Builtins.lc 503:39-503:56 Type
@@ -2362,6 +2444,8 @@ testdata/Builtins.lc 504:1-504:12 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float}
2362testdata/Builtins.lc 504:34-504:57 Type 2444testdata/Builtins.lc 504:34-504:57 Type
2363testdata/Builtins.lc 504:34-504:72 Type 2445testdata/Builtins.lc 504:34-504:72 Type
2364testdata/Builtins.lc 504:35-504:36 V3 2446testdata/Builtins.lc 504:35-504:36 V3
2447testdata/Builtins.lc 504:35-504:38 Type->Type
2448testdata/Builtins.lc 504:37-504:38 Type -> Type->Type
2365testdata/Builtins.lc 504:39-504:48 Nat -> Type->Type 2449testdata/Builtins.lc 504:39-504:48 Nat -> Type->Type
2366testdata/Builtins.lc 504:39-504:50 Type->Type 2450testdata/Builtins.lc 504:39-504:50 Type->Type
2367testdata/Builtins.lc 504:39-504:56 Type 2451testdata/Builtins.lc 504:39-504:56 Type
@@ -2509,16 +2593,20 @@ testdata/Builtins.lc 515:35-515:38 Type->Type
2509testdata/Builtins.lc 515:35-515:40 Type 2593testdata/Builtins.lc 515:35-515:40 Type
2510testdata/Builtins.lc 515:39-515:40 V7 2594testdata/Builtins.lc 515:39-515:40 V7
2511testdata/Builtins.lc 515:42-515:43 V6 2595testdata/Builtins.lc 515:42-515:43 V6
2596testdata/Builtins.lc 515:42-515:45 Type->Type
2512testdata/Builtins.lc 515:42-515:59 Type 2597testdata/Builtins.lc 515:42-515:59 Type
2513testdata/Builtins.lc 515:42-515:97 Type 2598testdata/Builtins.lc 515:42-515:97 Type
2599testdata/Builtins.lc 515:44-515:45 Type -> Type->Type
2514testdata/Builtins.lc 515:46-515:55 Nat -> Type->Type 2600testdata/Builtins.lc 515:46-515:55 Nat -> Type->Type
2515testdata/Builtins.lc 515:46-515:57 Type->Type 2601testdata/Builtins.lc 515:46-515:57 Type->Type
2516testdata/Builtins.lc 515:46-515:59 Type 2602testdata/Builtins.lc 515:46-515:59 Type
2517testdata/Builtins.lc 515:56-515:57 V4 2603testdata/Builtins.lc 515:56-515:57 V4
2518testdata/Builtins.lc 515:58-515:59 Type 2604testdata/Builtins.lc 515:58-515:59 Type
2519testdata/Builtins.lc 515:61-515:62 V3 2605testdata/Builtins.lc 515:61-515:62 V3
2606testdata/Builtins.lc 515:61-515:64 Type->Type
2520testdata/Builtins.lc 515:61-515:81 Type 2607testdata/Builtins.lc 515:61-515:81 Type
2521testdata/Builtins.lc 515:61-515:97 Type 2608testdata/Builtins.lc 515:61-515:97 Type
2609testdata/Builtins.lc 515:63-515:64 Type -> Type->Type
2522testdata/Builtins.lc 515:65-515:74 Nat -> Type->Type 2610testdata/Builtins.lc 515:65-515:74 Nat -> Type->Type
2523testdata/Builtins.lc 515:65-515:76 Type->Type 2611testdata/Builtins.lc 515:65-515:76 Type->Type
2524testdata/Builtins.lc 515:65-515:81 Type 2612testdata/Builtins.lc 515:65-515:81 Type
@@ -2534,6 +2622,8 @@ testdata/Builtins.lc 516:12-516:24 {a} -> {b} -> {c : a ~ MatVecScalarElem b} -
2534testdata/Builtins.lc 516:34-516:58 Type 2622testdata/Builtins.lc 516:34-516:58 Type
2535testdata/Builtins.lc 516:34-516:76 Type 2623testdata/Builtins.lc 516:34-516:76 Type
2536testdata/Builtins.lc 516:35-516:36 V3 2624testdata/Builtins.lc 516:35-516:36 V3
2625testdata/Builtins.lc 516:35-516:38 Type->Type
2626testdata/Builtins.lc 516:37-516:38 Type -> Type->Type
2537testdata/Builtins.lc 516:39-516:55 Type->Type 2627testdata/Builtins.lc 516:39-516:55 Type->Type
2538testdata/Builtins.lc 516:39-516:57 Type 2628testdata/Builtins.lc 516:39-516:57 Type
2539testdata/Builtins.lc 516:56-516:57 V1 2629testdata/Builtins.lc 516:56-516:57 V1
@@ -2548,6 +2638,8 @@ testdata/Builtins.lc 518:21-518:31 {a} -> {b:Nat} -> {c : a ~ VecScalar b Float
2548testdata/Builtins.lc 519:34-519:57 Type 2638testdata/Builtins.lc 519:34-519:57 Type
2549testdata/Builtins.lc 519:34-519:67 Type 2639testdata/Builtins.lc 519:34-519:67 Type
2550testdata/Builtins.lc 519:35-519:36 V3 2640testdata/Builtins.lc 519:35-519:36 V3
2641testdata/Builtins.lc 519:35-519:38 Type->Type
2642testdata/Builtins.lc 519:37-519:38 Type -> Type->Type
2551testdata/Builtins.lc 519:39-519:48 Nat -> Type->Type 2643testdata/Builtins.lc 519:39-519:48 Nat -> Type->Type
2552testdata/Builtins.lc 519:39-519:50 Type->Type 2644testdata/Builtins.lc 519:39-519:50 Type->Type
2553testdata/Builtins.lc 519:39-519:56 Type 2645testdata/Builtins.lc 519:39-519:56 Type
diff --git a/testdata/Internals.out b/testdata/Internals.out
index f55a02c2..a3430051 100644
--- a/testdata/Internals.out
+++ b/testdata/Internals.out
@@ -103,143 +103,147 @@ testdata/Internals.lc 42:24-42:28 Type
103testdata/Internals.lc 42:36-42:37 Type 103testdata/Internals.lc 42:36-42:37 Type
104testdata/Internals.lc 42:36-42:46 Type 104testdata/Internals.lc 42:36-42:46 Type
105testdata/Internals.lc 42:45-42:46 Type 105testdata/Internals.lc 42:45-42:46 Type
106testdata/Internals.lc 47:1-47:4 Unit -> Unit->Unit 106testdata/Internals.lc 44:6-44:11 Type -> Type->Type
107testdata/Internals.lc 47:8-47:12 Type 107testdata/Internals.lc 44:14-44:18 a:Type -> a -> a->Type
108testdata/Internals.lc 47:16-47:20 Type 108testdata/Internals.lc 44:14-44:23 Type -> Type->Type
109testdata/Internals.lc 47:16-47:28 Type 109testdata/Internals.lc 44:19-44:23 Type
110testdata/Internals.lc 47:24-47:28 Type 110testdata/Internals.lc 49:1-49:4 Unit -> Unit->Unit
111testdata/Internals.lc 50:6-50:9 Type 111testdata/Internals.lc 49:8-49:12 Type
112testdata/Internals.lc 51:6-51:10 Type 112testdata/Internals.lc 49:16-49:20 Type
113testdata/Internals.lc 52:6-52:11 Type 113testdata/Internals.lc 49:16-49:28 Type
114testdata/Internals.lc 49:24-49:28 Type
115testdata/Internals.lc 52:6-52:9 Type
114testdata/Internals.lc 53:6-53:10 Type 116testdata/Internals.lc 53:6-53:10 Type
117testdata/Internals.lc 54:6-54:11 Type
115testdata/Internals.lc 55:6-55:10 Type 118testdata/Internals.lc 55:6-55:10 Type
116testdata/Internals.lc 55:6-55:25 Type 119testdata/Internals.lc 57:6-57:10 Type
117testdata/Internals.lc 55:13-55:18 Bool 120testdata/Internals.lc 57:6-57:25 Type
118testdata/Internals.lc 55:21-55:25 Bool 121testdata/Internals.lc 57:13-57:18 Bool
119testdata/Internals.lc 57:6-57:14 Type 122testdata/Internals.lc 57:21-57:25 Bool
120testdata/Internals.lc 57:6-57:29 Type 123testdata/Internals.lc 59:6-59:14 Type
121testdata/Internals.lc 57:17-57:19 Ordering 124testdata/Internals.lc 59:6-59:29 Type
122testdata/Internals.lc 57:22-57:24 Ordering 125testdata/Internals.lc 59:17-59:19 Ordering
123testdata/Internals.lc 57:27-57:29 Ordering 126testdata/Internals.lc 59:22-59:24 Ordering
124testdata/Internals.lc 60:1-60:14 Int->Word 127testdata/Internals.lc 59:27-59:29 Ordering
125testdata/Internals.lc 60:24-60:27 Type 128testdata/Internals.lc 62:1-62:14 Int->Word
126testdata/Internals.lc 60:33-60:37 Type
127testdata/Internals.lc 61:1-61:15 Int->Float
128testdata/Internals.lc 61:24-61:27 Type
129testdata/Internals.lc 61:33-61:38 Type
130testdata/Internals.lc 62:1-62:15 Int -> Int->Ordering
131testdata/Internals.lc 62:24-62:27 Type 129testdata/Internals.lc 62:24-62:27 Type
132testdata/Internals.lc 62:33-62:36 Type 130testdata/Internals.lc 62:33-62:37 Type
133testdata/Internals.lc 62:33-62:50 Type 131testdata/Internals.lc 63:1-63:15 Int->Float
134testdata/Internals.lc 62:42-62:50 Type 132testdata/Internals.lc 63:24-63:27 Type
135testdata/Internals.lc 63:1-63:16 Word -> Word->Ordering 133testdata/Internals.lc 63:33-63:38 Type
136testdata/Internals.lc 63:24-63:28 Type 134testdata/Internals.lc 64:1-64:15 Int -> Int->Ordering
137testdata/Internals.lc 63:33-63:37 Type 135testdata/Internals.lc 64:24-64:27 Type
138testdata/Internals.lc 63:33-63:50 Type 136testdata/Internals.lc 64:33-64:36 Type
139testdata/Internals.lc 63:42-63:50 Type
140testdata/Internals.lc 64:1-64:17 Float -> Float->Ordering
141testdata/Internals.lc 64:24-64:29 Type
142testdata/Internals.lc 64:33-64:38 Type
143testdata/Internals.lc 64:33-64:50 Type 137testdata/Internals.lc 64:33-64:50 Type
144testdata/Internals.lc 64:42-64:50 Type 138testdata/Internals.lc 64:42-64:50 Type
145testdata/Internals.lc 65:1-65:16 Char -> Char->Ordering 139testdata/Internals.lc 65:1-65:16 Word -> Word->Ordering
146testdata/Internals.lc 65:24-65:28 Type 140testdata/Internals.lc 65:24-65:28 Type
147testdata/Internals.lc 65:33-65:37 Type 141testdata/Internals.lc 65:33-65:37 Type
148testdata/Internals.lc 65:33-65:50 Type 142testdata/Internals.lc 65:33-65:50 Type
149testdata/Internals.lc 65:42-65:50 Type 143testdata/Internals.lc 65:42-65:50 Type
150testdata/Internals.lc 66:1-66:18 String -> String->Ordering 144testdata/Internals.lc 66:1-66:17 Float -> Float->Ordering
151testdata/Internals.lc 66:24-66:30 Type 145testdata/Internals.lc 66:24-66:29 Type
152testdata/Internals.lc 66:34-66:40 Type 146testdata/Internals.lc 66:33-66:38 Type
153testdata/Internals.lc 66:34-66:52 Type 147testdata/Internals.lc 66:33-66:50 Type
154testdata/Internals.lc 66:44-66:52 Type 148testdata/Internals.lc 66:42-66:50 Type
155testdata/Internals.lc 67:1-67:14 Int->Int 149testdata/Internals.lc 67:1-67:16 Char -> Char->Ordering
156testdata/Internals.lc 67:24-67:27 Type 150testdata/Internals.lc 67:24-67:28 Type
157testdata/Internals.lc 67:33-67:36 Type 151testdata/Internals.lc 67:33-67:37 Type
158testdata/Internals.lc 68:1-68:15 Word->Word 152testdata/Internals.lc 67:33-67:50 Type
159testdata/Internals.lc 68:24-68:28 Type 153testdata/Internals.lc 67:42-67:50 Type
160testdata/Internals.lc 68:33-68:37 Type 154testdata/Internals.lc 68:1-68:18 String -> String->Ordering
161testdata/Internals.lc 69:1-69:16 Float->Float 155testdata/Internals.lc 68:24-68:30 Type
162testdata/Internals.lc 69:24-69:29 Type 156testdata/Internals.lc 68:34-68:40 Type
163testdata/Internals.lc 69:33-69:38 Type 157testdata/Internals.lc 68:34-68:52 Type
164testdata/Internals.lc 70:1-70:11 Int -> Int->Int 158testdata/Internals.lc 68:44-68:52 Type
165testdata/Internals.lc 70:24-70:27 Type 159testdata/Internals.lc 69:1-69:14 Int->Int
166testdata/Internals.lc 70:33-70:36 Type 160testdata/Internals.lc 69:24-69:27 Type
167testdata/Internals.lc 70:33-70:45 Type 161testdata/Internals.lc 69:33-69:36 Type
168testdata/Internals.lc 70:42-70:45 Type 162testdata/Internals.lc 70:1-70:15 Word->Word
169testdata/Internals.lc 71:1-71:11 Int -> Int->Int 163testdata/Internals.lc 70:24-70:28 Type
170testdata/Internals.lc 71:24-71:27 Type 164testdata/Internals.lc 70:33-70:37 Type
171testdata/Internals.lc 71:33-71:36 Type 165testdata/Internals.lc 71:1-71:16 Float->Float
172testdata/Internals.lc 71:33-71:45 Type 166testdata/Internals.lc 71:24-71:29 Type
173testdata/Internals.lc 71:42-71:45 Type 167testdata/Internals.lc 71:33-71:38 Type
174testdata/Internals.lc 72:1-72:11 Int -> Int->Int 168testdata/Internals.lc 72:1-72:11 Int -> Int->Int
175testdata/Internals.lc 72:24-72:27 Type 169testdata/Internals.lc 72:24-72:27 Type
176testdata/Internals.lc 72:33-72:36 Type 170testdata/Internals.lc 72:33-72:36 Type
177testdata/Internals.lc 72:33-72:45 Type 171testdata/Internals.lc 72:33-72:45 Type
178testdata/Internals.lc 72:42-72:45 Type 172testdata/Internals.lc 72:42-72:45 Type
179testdata/Internals.lc 73:1-73:14 Float->Float 173testdata/Internals.lc 73:1-73:11 Int -> Int->Int
180testdata/Internals.lc 73:24-73:29 Type 174testdata/Internals.lc 73:24-73:27 Type
181testdata/Internals.lc 73:33-73:38 Type 175testdata/Internals.lc 73:33-73:36 Type
182testdata/Internals.lc 74:1-74:10 Float->Int 176testdata/Internals.lc 73:33-73:45 Type
183testdata/Internals.lc 74:24-74:29 Type 177testdata/Internals.lc 73:42-73:45 Type
178testdata/Internals.lc 74:1-74:11 Int -> Int->Int
179testdata/Internals.lc 74:24-74:27 Type
184testdata/Internals.lc 74:33-74:36 Type 180testdata/Internals.lc 74:33-74:36 Type
185testdata/Internals.lc 77:19-77:23 Type 181testdata/Internals.lc 74:33-74:45 Type
186testdata/Internals.lc 77:19-77:38 Type 182testdata/Internals.lc 74:42-74:45 Type
187testdata/Internals.lc 77:27-77:28 V2 183testdata/Internals.lc 75:1-75:14 Float->Float
188testdata/Internals.lc 77:27-77:38 Type 184testdata/Internals.lc 75:24-75:29 Type
189testdata/Internals.lc 77:32-77:33 Type 185testdata/Internals.lc 75:33-75:38 Type
190testdata/Internals.lc 77:32-77:38 Type 186testdata/Internals.lc 76:1-76:10 Float->Int
191testdata/Internals.lc 77:37-77:38 Type 187testdata/Internals.lc 76:24-76:29 Type
192testdata/Internals.lc 78:1-78:15 {a} -> Bool -> a -> a->a 188testdata/Internals.lc 76:33-76:36 Type
193testdata/Internals.lc 78:16-78:20 Bool 189testdata/Internals.lc 79:19-79:23 Type
194testdata/Internals.lc 78:16-79:29 Bool -> V1 -> V2->V3 | V1 -> V2->V3 | V2->V3 | V3 190testdata/Internals.lc 79:19-79:38 Type
195testdata/Internals.lc 78:28-78:29 V3 191testdata/Internals.lc 79:27-79:28 V2
196testdata/Internals.lc 78:28-79:29 Bool->V4 192testdata/Internals.lc 79:27-79:38 Type
197testdata/Internals.lc 79:28-79:29 V4 193testdata/Internals.lc 79:32-79:33 Type
198testdata/Internals.lc 82:7-82:10 Type->Type 194testdata/Internals.lc 79:32-79:38 Type
199testdata/Internals.lc 82:7-83:22 Type 195testdata/Internals.lc 79:37-79:38 Type
200testdata/Internals.lc 82:7-84:32 Type 196testdata/Internals.lc 80:1-80:15 {a} -> Bool -> a -> a->a
201testdata/Internals.lc 82:7-85:19 Type 197testdata/Internals.lc 80:16-80:20 Bool
202testdata/Internals.lc 83:3-83:10 {a} -> {b : Num a} -> Int->a 198testdata/Internals.lc 80:16-81:29 Bool -> V1 -> V2->V3 | V1 -> V2->V3 | V2->V3 | V3
203testdata/Internals.lc 83:14-83:17 Type 199testdata/Internals.lc 80:28-80:29 V3
204testdata/Internals.lc 83:14-83:22 Type 200testdata/Internals.lc 80:28-81:29 Bool->V4
205testdata/Internals.lc 83:21-83:22 Type 201testdata/Internals.lc 81:28-81:29 V4
206testdata/Internals.lc 84:3-84:10 {a} -> {b : Num a} -> a -> a->Ordering 202testdata/Internals.lc 84:7-84:10 Type->Type
207testdata/Internals.lc 84:14-84:15 Type 203testdata/Internals.lc 84:7-85:22 Type
208testdata/Internals.lc 84:14-84:32 Type 204testdata/Internals.lc 84:7-86:32 Type
209testdata/Internals.lc 84:19-84:20 Type 205testdata/Internals.lc 84:7-87:19 Type
210testdata/Internals.lc 84:19-84:32 Type 206testdata/Internals.lc 85:3-85:10 {a} -> {b : Num a} -> Int->a
211testdata/Internals.lc 84:24-84:32 Type 207testdata/Internals.lc 85:14-85:17 Type
212testdata/Internals.lc 85:3-85:9 {a} -> {b : Num a} -> a->a 208testdata/Internals.lc 85:14-85:22 Type
213testdata/Internals.lc 85:13-85:14 Type 209testdata/Internals.lc 85:21-85:22 Type
214testdata/Internals.lc 85:13-85:19 Type 210testdata/Internals.lc 86:3-86:10 {a} -> {b : Num a} -> a -> a->Ordering
215testdata/Internals.lc 85:18-85:19 Type 211testdata/Internals.lc 86:14-86:15 Type
216testdata/Internals.lc 87:14-87:17 Type 212testdata/Internals.lc 86:14-86:32 Type
217testdata/Internals.lc 87:14-88:20 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3 213testdata/Internals.lc 86:19-86:20 Type
218testdata/Internals.lc 87:14-89:27 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering 214testdata/Internals.lc 86:19-86:32 Type
219testdata/Internals.lc 87:14-90:26 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3 215testdata/Internals.lc 86:24-86:32 Type
220testdata/Internals.lc 87:14-95:19 Type | Type->Type 216testdata/Internals.lc 87:3-87:9 {a} -> {b : Num a} -> a->a
221testdata/Internals.lc 87:14-96:27 {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a 217testdata/Internals.lc 87:13-87:14 Type
222testdata/Internals.lc 87:14-97:29 {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering 218testdata/Internals.lc 87:13-87:19 Type
223testdata/Internals.lc 87:14-98:28 {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a 219testdata/Internals.lc 87:18-87:19 Type
224testdata/Internals.lc 88:13-88:20 Int->Int 220testdata/Internals.lc 89:14-89:17 Type
225testdata/Internals.lc 88:19-88:20 Int 221testdata/Internals.lc 89:14-90:20 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
226testdata/Internals.lc 89:13-89:27 Int -> Int->Ordering 222testdata/Internals.lc 89:14-91:27 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
227testdata/Internals.lc 90:13-90:26 Int->Int 223testdata/Internals.lc 89:14-92:26 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
228testdata/Internals.lc 91:14-91:18 Type 224testdata/Internals.lc 89:14-97:19 Type | Type->Type
229testdata/Internals.lc 91:14-92:26 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3 225testdata/Internals.lc 89:14-98:27 {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a
230testdata/Internals.lc 91:14-93:28 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering 226testdata/Internals.lc 89:14-99:29 {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering
231testdata/Internals.lc 91:14-94:27 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3 227testdata/Internals.lc 89:14-100:28 {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a
232testdata/Internals.lc 91:14-95:19 Type 228testdata/Internals.lc 90:13-90:20 Int->Int
233testdata/Internals.lc 91:14-96:27 {a : Num V0} -> Int->V2 229testdata/Internals.lc 90:19-90:20 Int
234testdata/Internals.lc 91:14-97:29 {a : Num V0} -> V1 -> V2->Ordering 230testdata/Internals.lc 91:13-91:27 Int -> Int->Ordering
235testdata/Internals.lc 91:14-98:28 {a : Num V0} -> V1->V2 231testdata/Internals.lc 92:13-92:26 Int->Int
236testdata/Internals.lc 92:13-92:26 Int->Word 232testdata/Internals.lc 93:14-93:18 Type
237testdata/Internals.lc 93:13-93:28 Word -> Word->Ordering 233testdata/Internals.lc 93:14-94:26 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
238testdata/Internals.lc 94:13-94:27 Word->Word 234testdata/Internals.lc 93:14-95:28 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
239testdata/Internals.lc 95:14-95:19 Type 235testdata/Internals.lc 93:14-96:27 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
240testdata/Internals.lc 95:14-96:27 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3 236testdata/Internals.lc 93:14-97:19 Type
241testdata/Internals.lc 95:14-97:29 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering 237testdata/Internals.lc 93:14-98:27 {a : Num V0} -> Int->V2
242testdata/Internals.lc 95:14-98:28 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3 238testdata/Internals.lc 93:14-99:29 {a : Num V0} -> V1 -> V2->Ordering
243testdata/Internals.lc 96:13-96:27 Int->Float 239testdata/Internals.lc 93:14-100:28 {a : Num V0} -> V1->V2
244testdata/Internals.lc 97:13-97:29 Float -> Float->Ordering 240testdata/Internals.lc 94:13-94:26 Int->Word
245testdata/Internals.lc 98:13-98:28 Float->Float 241testdata/Internals.lc 95:13-95:28 Word -> Word->Ordering
242testdata/Internals.lc 96:13-96:27 Word->Word
243testdata/Internals.lc 97:14-97:19 Type
244testdata/Internals.lc 97:14-98:27 ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
245testdata/Internals.lc 97:14-99:29 ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
246testdata/Internals.lc 97:14-100:28 ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
247testdata/Internals.lc 98:13-98:27 Int->Float
248testdata/Internals.lc 99:13-99:29 Float -> Float->Ordering
249testdata/Internals.lc 100:13-100:28 Float->Float
diff --git a/testdata/Prelude.out b/testdata/Prelude.out
index 1ce1896f..4d590c76 100644
--- a/testdata/Prelude.out
+++ b/testdata/Prelude.out
@@ -400,7 +400,9 @@ testdata/Prelude.lc 165:32-165:52 Type->Type
400testdata/Prelude.lc 165:34-165:37 {a} -> {b : Eq a} -> a -> a->Bool 400testdata/Prelude.lc 165:34-165:37 {a} -> {b : Eq a} -> a -> a->Bool
401testdata/Prelude.lc 165:38-165:40 V6 401testdata/Prelude.lc 165:38-165:40 V6
402testdata/Prelude.lc 165:46-165:47 V12 402testdata/Prelude.lc 165:46-165:47 V12
403testdata/Prelude.lc 165:46-165:49 Type->Type
403testdata/Prelude.lc 165:46-165:52 Type 404testdata/Prelude.lc 165:46-165:52 Type
405testdata/Prelude.lc 165:48-165:49 Type -> Type->Type
404testdata/Prelude.lc 165:50-165:52 V4 406testdata/Prelude.lc 165:50-165:52 V4
405testdata/Prelude.lc 165:58-165:64 V12 407testdata/Prelude.lc 165:58-165:64 V12
406testdata/Prelude.lc 165:65-165:66 V13 408testdata/Prelude.lc 165:65-165:66 V13
diff --git a/testdata/language-features/basic-values/def05.reject.out b/testdata/language-features/basic-values/def05.reject.out
index f24dbe10..d260d164 100644
--- a/testdata/language-features/basic-values/def05.reject.out
+++ b/testdata/language-features/basic-values/def05.reject.out
@@ -1,4 +1,4 @@
1"testdata/language-features/basic-values/def05.reject.lc" (line 4, column 1): 1"testdata/language-features/basic-values/def05.reject.lc" (line 4, column 1):
2unexpected end of input 2unexpected end of input
3expecting projection, swizzling, "@", char literal, literal string, float literal, "#", natural, "_", "'", identifier, uppercase ident, "[", "(", "{", "let", symbols, op symbols, backquoted ident, expression, lambda, "::", "~", "->", "=>", "where", "data", "class", "instance", type family, type instance, "type", typed ident, "infix", "infixl", "infixr", operator definition, lhs or pattern 3expecting projection, swizzling, "@", char literal, literal string, float literal, "#", natural, "_", "'", identifier, uppercase ident, "[", "(", "{", "let", symbols, op symbols, backquoted ident, "~", expression, lambda, "::", "->", "=>", "where", "data", "class", "instance", type family, type instance, "type", typed ident, "infix", "infixl", "infixr", operator definition, lhs or pattern
4different number of arguments of fun at testdata/language-features/basic-values/def05.reject.lc 1:1-1:4 \ No newline at end of file 4different number of arguments of fun at testdata/language-features/basic-values/def05.reject.lc 1:1-1:4 \ No newline at end of file
diff --git a/testdata/language-features/basic-values/def06.reject.out b/testdata/language-features/basic-values/def06.reject.out
index 32761406..f80e12f8 100644
--- a/testdata/language-features/basic-values/def06.reject.out
+++ b/testdata/language-features/basic-values/def06.reject.out
@@ -1,4 +1,4 @@
1"testdata/language-features/basic-values/def06.reject.lc" (line 5, column 1): 1"testdata/language-features/basic-values/def06.reject.lc" (line 5, column 1):
2unexpected end of input 2unexpected end of input
3expecting projection, swizzling, "@", char literal, literal string, float literal, "#", natural, "_", "'", identifier, uppercase ident, "[", "(", "{", "let", symbols, op symbols, backquoted ident, expression, lambda, "::", "~", "->", "=>", "where", "data", "class", "instance", type family, type instance, "type", typed ident, "infix", "infixl", "infixr", operator definition, lhs or pattern 3expecting projection, swizzling, "@", char literal, literal string, float literal, "#", natural, "_", "'", identifier, uppercase ident, "[", "(", "{", "let", symbols, op symbols, backquoted ident, "~", expression, lambda, "::", "->", "=>", "where", "data", "class", "instance", type family, type instance, "type", typed ident, "infix", "infixl", "infixr", operator definition, lhs or pattern
4different number of arguments of fun2 at testdata/language-features/basic-values/def06.reject.lc 1:1-1:5 \ No newline at end of file 4different number of arguments of fun2 at testdata/language-features/basic-values/def06.reject.lc 1:1-1:5 \ No newline at end of file
diff --git a/testdata/language-features/basic-values/redefine03.reject.out b/testdata/language-features/basic-values/redefine03.reject.out
index aa37ecee..f8e236ab 100644
--- a/testdata/language-features/basic-values/redefine03.reject.out
+++ b/testdata/language-features/basic-values/redefine03.reject.out
@@ -1,4 +1,4 @@
1"testdata/language-features/basic-values/redefine03.reject.lc" (line 4, column 1): 1"testdata/language-features/basic-values/redefine03.reject.lc" (line 4, column 1):
2unexpected end of input 2unexpected end of input
3expecting projection, swizzling, "@", char literal, literal string, float literal, "#", natural, "_", "'", identifier, uppercase ident, "[", "(", "{", "let", symbols, op symbols, backquoted ident, expression, lambda, "::", "~", "->", "=>", "where", "data", "class", "instance", type family, type instance, "type", typed ident, "infix", "infixl", "infixr", operator definition, lhs or pattern 3expecting projection, swizzling, "@", char literal, literal string, float literal, "#", natural, "_", "'", identifier, uppercase ident, "[", "(", "{", "let", symbols, op symbols, backquoted ident, "~", expression, lambda, "::", "->", "=>", "where", "data", "class", "instance", type family, type instance, "type", typed ident, "infix", "infixl", "infixr", operator definition, lhs or pattern
4redefined x at testdata/language-features/basic-values/redefine03.reject.lc 2:9-2:10 \ No newline at end of file 4redefined x at testdata/language-features/basic-values/redefine03.reject.lc 2:9-2:10 \ No newline at end of file
diff --git a/testdata/language-features/guard/guard10.reject.out b/testdata/language-features/guard/guard10.reject.out
index d998f2d5..16c0debe 100644
--- a/testdata/language-features/guard/guard10.reject.out
+++ b/testdata/language-features/guard/guard10.reject.out
@@ -1,3 +1,3 @@
1"testdata/language-features/guard/guard10.reject.lc" (line 2, column 1): 1"testdata/language-features/guard/guard10.reject.lc" (line 2, column 1):
2unexpected '|' 2unexpected '|'
3expecting projection, swizzling, "@", char literal, literal string, float literal, "#", natural, "_", "'", identifier, uppercase ident, "[", "(", "{", "let", symbols, op symbols, backquoted ident, expression, lambda, "::", "~", "->", "=>", "|", "data", "class", "instance", type family, type instance, "type", typed ident, "infix", "infixl", "infixr", operator definition, lhs, pattern or end of input \ No newline at end of file 3expecting projection, swizzling, "@", char literal, literal string, float literal, "#", natural, "_", "'", identifier, uppercase ident, "[", "(", "{", "let", symbols, op symbols, backquoted ident, "~", expression, lambda, "::", "->", "=>", "|", "data", "class", "instance", type family, type instance, "type", typed ident, "infix", "infixl", "infixr", operator definition, lhs, pattern or end of input \ No newline at end of file
diff --git a/testdata/listcompr01.reject.out b/testdata/listcompr01.reject.out
index b43b8f71..1d3a6936 100644
--- a/testdata/listcompr01.reject.out
+++ b/testdata/listcompr01.reject.out
@@ -1,3 +1,3 @@
1"testdata/listcompr01.reject.lc" (line 6, column 42): 1"testdata/listcompr01.reject.lc" (line 6, column 42):
2unexpected ',' 2unexpected ','
3expecting projection, swizzling, "@", char literal, literal string, float literal, "#", natural, "_", "'", identifier, uppercase ident, "[", "(", "{", "let", symbols, op symbols, backquoted ident, expression, lambda, "::", "~", "->", "=>", "where", "data", "class", "instance", type family, type instance, "type", typed ident, "infix", "infixl", "infixr", operator definition, lhs, pattern or end of input \ No newline at end of file 3expecting projection, swizzling, "@", char literal, literal string, float literal, "#", natural, "_", "'", identifier, uppercase ident, "[", "(", "{", "let", symbols, op symbols, backquoted ident, "~", expression, lambda, "::", "->", "=>", "where", "data", "class", "instance", type family, type instance, "type", typed ident, "infix", "infixl", "infixr", operator definition, lhs, pattern or end of input \ No newline at end of file