refactoring: use less STyped

3 files changed, 241 insertions, 249 deletions

diff --git a/lc/Internals.lc b/lc/Internals.lc
index 5c359e0a..aedb62fc 100644
--- a/lc/Internals.lc
+++ b/lc/Internals.lc
@@ -2,6 +2,9 @@
 -- declarations of builtin functions and data types used by the compiler
 module Internals where
 
+-- used for type annotations
+typeAnn x = x
+
 undefined :: forall (a :: Type) . a
 
 primFix :: forall (a :: Type) . (a -> a) -> a
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 60ac7819..90b0d34f 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -13,6 +13,7 @@
 {-# OPTIONS_GHC -fno-warn-overlapping-patterns #-}  -- TODO: remove
 {-# OPTIONS_GHC -fno-warn-unused-binds #-}  -- TODO: remove
 {-# OPTIONS_GHC -fno-warn-orphans #-}  -- instance NFData SourcePos
+-- {-# OPTIONS_GHC -O0 #-}
 module LambdaCube.Compiler.Infer
     ( Binder (..), SName, Lit(..), Visibility(..), FunName(..), CaseFunName(..), ConName(..), TyConName(..), Export(..), ModuleR(..)
     , Exp (..), GlobalEnv
@@ -95,6 +96,7 @@ dsInfo = asks fst
 
 -------------------------------------------------------------------------------- lexing
 
+{-# NOINLINE lexer #-}
 lexer :: Pa.GenTokenParser (IndentStream (CharIndentStream String)) SourcePos InnerP
 lexer = makeTokenParser lexeme $ makeIndentLanguageDef style
   where
@@ -394,20 +396,18 @@ data Visibility = Hidden | Visible
 
 sLit a = STyped mempty (ELit a, litType a)
 pattern Primitive n mf t <- Let n mf (Just t) _ (SBuiltin "undefined") where Primitive n mf t = Let n mf (Just t) (map fst $ fst $ getParamsS t) $ SBuiltin "undefined"
-pattern SType <- STyped _ (TType, TType) where SType = STyped (debugSI "pattern SType") (TType, TType)
+pattern SType = SBuiltin "'Type"
 pattern SPi  h a b <- SBind _ (BPi  h) _ a b where SPi  h a b = sBind (BPi  h) (SData (debugSI "patternSPi2", "pattern_spi_name")) a b
 pattern SLam h a b <- SBind _ (BLam h) _ a b where SLam h a b = sBind (BLam h) (SData (debugSI "patternSLam2", "pattern_slam_name")) a b
 pattern Wildcard t <- SBind _ BMeta _ t (SVar _ 0) where Wildcard t = sBind BMeta (SData (debugSI "pattern Wildcard2", "pattern_wildcard_name")) t (SVar (debugSI "pattern Wildcard2", ".wc") 0)
 pattern Wildcard_ si t <- SBind _ BMeta _ t (SVar (si, _) 0)
-pattern SAppH a b <- SApp _ Hidden a b where SAppH a b = sApp Hidden a b
-pattern SAppV a b <- SApp _ Visible a b where SAppV a b = sApp Visible a b
+pattern SApp' h a b <- SApp _ h a b where SApp' h a b = sApp h a b
+pattern SAppH a b = SApp' Hidden a b
+pattern SAppV a b = SApp' Visible a b
 pattern SAppV2 f a b    = f `SAppV` a `SAppV` b
 pattern SLamV a = SLam Visible (Wildcard SType) a
-pattern       SAnn a t <- STyped _ (Lam Visible TType (Lam Visible (Var 0) (Var 0)), TType :~> Var 0 :~> Var 1) `SAppV` t `SAppV` a  --  a :: t ~~> id t a
-        where SAnn a t = STyped (debugSI "pattern SAnn") (Lam Visible TType (Lam Visible (Var 0) (Var 0)), TType :~> Var 0 :~> Var 1) `SAppV` t `SAppV` a
-pattern       TyType a <- STyped _ (Lam Visible TType (Var 0), TType :~> TType) `SAppV` a
-        where TyType a = STyped mempty (Lam Visible TType (Var 0), TType :~> TType) `SAppV` a
-    -- same as  (a :: TType)     --  a :: TType   ~~>   (\(x :: TType) -> x) a
+pattern SAnn a t = SBuiltin "typeAnn" `SAppH` t `SAppV` a
+pattern TyType a = SAnn a SType
 pattern SLabelEnd a     = SBuiltin "labelend" `SAppV` a
 
 pattern SBuiltin s <- SGlobal (_, s) where SBuiltin s = SGlobal (debugSI $ "builtin " ++ s, s)
@@ -607,7 +607,7 @@ toNat n | n > 0 = SAppV (SBuiltin "Succ") $ toNat (n-1)
 addForalls :: Extensions -> [SName] -> SExp -> SExp
 addForalls exs defined x = foldl f x [v | v@(vh:_) <- reverse $ freeS x, v `notElem'` defined, isLower vh || NoConstructorNamespace `elem` exs]
   where
-    f e v = SPi Hidden (Wildcard SType) $ substSG0 v e
+    f e v = SPi Hidden (Wildcard SType) $ substSG0 (mempty, v) e
 {-
 defined defs = ("'Type":) $ flip foldMap defs $ \case
     TypeAnn (_, x) _ -> [x]
@@ -958,9 +958,9 @@ valueDef = do
 mkLets :: Bool -> DesugarInfo -> [Stmt]{-where block-} -> SExp{-main expression-} -> SExp{-big let with lambdas; replaces global names with de bruijn indices-}
 mkLets _ _ [] e = e
 mkLets False ge (Let n _ mt ar (downS 0 -> Just x): ds) e
-    = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 (snd n) $ mkLets False ge ds e)
+    = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 n $ mkLets False ge ds e)
 mkLets True ge (Let n _ mt ar (downS 0 -> Just x): ds) e
-    = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 (snd n) $ mkLets True ge ds e)
+    = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 n $ mkLets True ge ds e)
 mkLets le ge (ValueDef p x: ds) e = patLam id ge p (dbff (getPVars p) $ mkLets le ge ds e) `SAppV` x    -- (p = e; f) -->  (\p -> f) e
 mkLets _ _ (x: ds) e = error $ "mkLets: " ++ show x
 
@@ -1786,25 +1786,32 @@ usedE i e
     | i >= maxDB e = False
     | otherwise = ((getAny .) . foldE ((Any .) . (==))) i e
 
-mapS = mapS_ (\si _ x -> SGlobal (si, x))
-mapS_ gg ff = mapS__ gg ff $ \sn i j -> case ff i $ Var j of
-            Var k -> SVar sn k
-            -- x -> STyped x -- todo
+mapS' = mapS__ (const . SGlobal)
 mapS__ gg f1 f2 h = g where
     g i = \case
         SApp si v a b -> SApp si v (g i a) (g i b)
         SLet x a b -> SLet x (g i a) (g (h i) b)
         SBind si k si' a b -> SBind si k si' (g i a) (g (h i) b)
         STyped si (x, t) -> STyped si (f1 i x, f1 i t)
-        SVar sn j -> f2 sn i j
-        SGlobal (si, x) -> gg si i x
+        SVar sn j -> f2 sn j i
+        SGlobal sn -> gg sn i
 
 rearrangeS :: (Int -> Int) -> SExp -> SExp
-rearrangeS f = mapS__ (\si _ x -> SGlobal (si,x)) (const id) (\sn i j -> SVar sn $ if j < i then j else i + f (j - i)) (+1) 0
+rearrangeS f = mapS' (const id){-todo-} (\sn j i -> SVar sn $ if j < i then j else i + f (j - i)) (+1) 0
 
-upS__ i n = mapS (`upE` n) (+1) i
+upS__ i n = mapS' (`upE` n) (\sn j i -> SVar sn $ if j < i then j else j+n) (+1) i
 upS = upS__ 0 1
 
+-- todo: review
+substS j x = mapS' (uncurry $ substE "substS") f2 ((+1) *** up1E 0) (j, x)
+  where
+    f2 sn j i = case uncurry (substE "substS'") i $ Var j of
+            Var k -> SVar sn k
+            x -> STyped (fst sn) (x, error "type of x"{-todo-})
+
+substSG j = mapS__ (\sn x -> if sn == j then SVar sn x else SGlobal sn) (const id) (\sn j -> const $ SVar sn j) (+1)
+substSG0 n = substSG n 0 . upS
+
 up1E i e | isClosed e = e
 up1E i e = case e of
     Var k -> Var $ if k >= i then k+1 else k
@@ -1825,22 +1832,11 @@ up1E i e = case e of
 
 upE i n = iterateN n (up1E i)
 
-substSS :: Int -> SExp -> SExp -> SExp
-substSS k x = mapS__ (\si _ x -> SGlobal (si, x)) (error "substSS") (\sn (i, x) j -> case compare j i of
-            EQ -> x
-            GT -> SVar sn $ j - 1
-            LT -> SVar sn j
-            ) ((+1) *** upS) (k, x)
-substS j x = mapS (uncurry $ substE "substS") ((+1) *** up1E 0) (j, x)
-substSG :: SName -> (SI -> SExp) -> SExp -> SExp
-substSG j = mapS_ (\si x i -> if i == j then x si else SGlobal (si, i)) (const id) (fmap upS)
-substSG0 n e = substSG n (\si -> SVar (si, n) 0) $ upS e
-
 dbf' = dbf_ 0
-dbf_ j xs e = foldl (\e (i, (si, n)) -> substSG n (\si -> SVar (si, n) i) e) e $ zip [j..] xs
+dbf_ j xs e = foldl (\e (i, sn) -> substSG sn i e) e $ zip [j..] xs
 
 dbff :: DBNames -> SExp -> SExp
-dbff ns e = foldr (substSG0 . snd) e ns
+dbff ns e = foldr substSG0 e ns
 
 substE err = substE_ (error $ "substE: todo: environment required in " ++ err)  -- todo: remove
 
@@ -1849,23 +1845,14 @@ substE_ te i x e | {-i >= maxDB e-} isClosed e = e
 substE_ te i x e = case e of
     Label lk z v -> label lk (substE "slab" i x z) $ substE_ te{-todo: label env?-} i x v
     Var k -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> x
-    Lam h a b -> let  -- question: is mutual recursion good here?
-            a' = substE_ te i x a
-            b' = substE_ (EBind2 (BLam h) a' te) (i+1) (up1E 0 x) b
-        in Lam h a' b'
-    Meta a b -> let  -- question: is mutual recursion good here?
-            a' = substE_ te i x a
-            b' = substE_ (EBind2 BMeta a' te) (i+1) (up1E 0 x) b
-        in Meta a' b'
-    Pi h a b -> let  -- question: is mutual recursion good here?
-            a' = substE_ te i x a
-            b' = substE_ (EBind2 (BPi h) a' te) (i+1) (up1E 0 x) b
-        in Pi h a' b'
-    Fun s as  -> eval te $ Fun s [substE_ te{-todo: precise env?-} i x a | a <- as]
-    CaseFun s as  -> eval te $ CaseFun s [substE_ te{-todo: precise env?-} i x a | a <- as]
-    TyCaseFun s as -> eval te $ TyCaseFun s [substE_ te{-todo: precise env?-} i x a | a <- as]
-    Con s as  -> Con s [substE_ te{-todo-} i x a | a <- as]
-    TyCon s as -> TyCon s [substE_ te{-todo-} i x a | a <- as]
+    Lam h a b -> Lam h (substE_ te i x a) (substE_ te (i+1) (up1E 0 x) b)
+    Meta a b  -> Meta (substE_ te i x a) (substE_ te (i+1) (up1E 0 x) b)
+    Pi h a b  -> Pi h (substE_ te i x a) (substE_ te (i+1) (up1E 0 x) b)
+    Fun s as  -> eval te $ Fun s $ substE_ te i x <$> as
+    CaseFun s as  -> eval te $ CaseFun s $ substE_ te i x <$> as
+    TyCaseFun s as -> eval te $ TyCaseFun s $ substE_ te i x <$> as
+    Con s as  -> Con s $ substE_ te i x <$> as
+    TyCon s as -> TyCon s $ substE_ te i x <$> as
     TType -> TType
     ELit l -> ELit l
     App a b  -> app_ (substE_ te i x a) (substE_ te i x b)  -- todo: precise env?
@@ -1981,10 +1968,10 @@ eval te = \case
 
     Fun n@(FunName "natElim" _ _) [a, z, s, Succ x] -> let      -- todo: replace let with better abstraction
                 sx = s `app_` x
-            in sx `app_` eval (EApp2 mempty Visible sx te) (Fun n [a, z, s, x])
+            in sx `app_` eval te (Fun n [a, z, s, x])
     FunN "natElim" [_, z, s, Zero] -> z
     Fun na@(FunName "finElim" _ _) [m, z, s, n, ConN "FSucc" [i, x]] -> let six = s `app_` i `app_` x-- todo: replace let with better abstraction
-        in six `app_` eval (EApp2 mempty Visible six te) (Fun na [m, z, s, i, x])
+        in six `app_` eval te (Fun na [m, z, s, i, x])
     FunN "finElim" [m, z, s, n, ConN "FZero" [i]] -> z `app_` i
 
     FunN "'TFFrameBuffer" [TyConN "'Image" [n, t]] -> TFrameBuffer n t
@@ -2192,7 +2179,7 @@ inferN tracelevel = infer  where
     checkN_ te e t
             -- temporal hack
         | x@(SGlobal (si, MatchName n)) `SAppV` SLamV (Wildcard_ siw _) `SAppV` a `SAppV` SVar siv v `SAppV` b <- e
-            = infer te $ x `SAppV` STyped mempty (Lam Visible TType $ substE "checkN" (v+1) (Var 0) $ up1E 0 t, TType :~> TType) `SAppV` a `SAppV` SVar siv v `SAppV` b
+            = infer te $ x `SAppV` SLam Visible SType (STyped mempty (substE "checkN" (v+1) (Var 0) $ up1E 0 t, TType)) `SAppV` a `SAppV` SVar siv v `SAppV` b
             -- temporal hack
         | x@(SGlobal (si, "'NatCase")) `SAppV` SLamV (Wildcard_ siw _) `SAppV` a `SAppV` b `SAppV` SVar siv v <- e
             = infer te $ x `SAppV` STyped mempty (Lam Visible TNat $ substE "checkN" (v+1) (Var 0) $ up1E 0 t, TNat :~> TType) `SAppV` a `SAppV` b `SAppV` SVar siv v
@@ -2228,7 +2215,7 @@ inferN tracelevel = infer  where
 -}
     checkSame te (Wildcard _) a = True
     checkSame te (SGlobal (_,"'Type")) TType = True
-    checkSame te (STyped _ (TType, TType)) TType = True
+    checkSame te SType TType = True
     checkSame te (SBind _ BMeta _ SType (STyped _ (Var 0, _))) a = True
     checkSame te a b = error $ "checkSame: " ++ show (a, b)
 
diff --git a/testdata/Internals.out b/testdata/Internals.out
index dc29d25e..9aea069f 100644
--- a/testdata/Internals.out
+++ b/testdata/Internals.out
@@ -1,207 +1,209 @@
 main is not found
 tooltips:
-testdata/Internals.lc 5:1-5:10  {a}->a
-testdata/Internals.lc 5:27-5:31  Type
-testdata/Internals.lc 5:35-5:36  Type
-testdata/Internals.lc 7:1-7:8  {a} -> a->a -> a
-testdata/Internals.lc 7:25-7:29  Type
-testdata/Internals.lc 7:33-7:46  Type
-testdata/Internals.lc 7:34-7:35  Type
-testdata/Internals.lc 7:39-7:40  Type
-testdata/Internals.lc 7:45-7:46  Type
-testdata/Internals.lc 9:6-9:10  Type
-testdata/Internals.lc 9:6-9:15  Type
-testdata/Internals.lc 9:13-9:15  Unit
-testdata/Internals.lc 10:6-10:12  Type
-testdata/Internals.lc 11:6-11:11  String->Type | Type
-testdata/Internals.lc 11:18-11:24  Type
-testdata/Internals.lc 14:6-14:12  Type
-testdata/Internals.lc 14:6-14:21  Type
-testdata/Internals.lc 14:15-14:21  Tuple0
-testdata/Internals.lc 15:6-15:12  Type | Type->Type
-testdata/Internals.lc 15:6-15:23  Type
-testdata/Internals.lc 15:6-15:25  Type
-testdata/Internals.lc 15:17-15:23  Tuple1 V2 | Type | {a} -> a -> Tuple1 a
-testdata/Internals.lc 15:24-15:25  Type
-testdata/Internals.lc 16:6-16:12  Type | Type -> Type->Type
-testdata/Internals.lc 16:6-16:25  Type
-testdata/Internals.lc 16:6-16:29  Type
-testdata/Internals.lc 16:19-16:25  Tuple2 V4 V3 | Type | {a} -> {b} -> a -> b -> Tuple2 a b
-testdata/Internals.lc 16:26-16:27  Type
-testdata/Internals.lc 16:28-16:29  Type
-testdata/Internals.lc 17:6-17:12  Type | Type -> Type -> Type->Type
-testdata/Internals.lc 17:6-17:27  Type
-testdata/Internals.lc 17:6-17:33  Type
-testdata/Internals.lc 17:21-17:27  Tuple3 V6 V5 V4 | Type | {a} -> {b} -> {c} -> a -> b -> c -> Tuple3 a b c
-testdata/Internals.lc 17:28-17:29  Type
-testdata/Internals.lc 17:30-17:31  Type
-testdata/Internals.lc 17:32-17:33  Type
-testdata/Internals.lc 18:6-18:12  Type | Type -> Type -> Type -> Type->Type
-testdata/Internals.lc 18:6-18:29  Type
-testdata/Internals.lc 18:6-18:37  Type
-testdata/Internals.lc 18:23-18:29  Tuple4 V8 V7 V6 V5 | Type | {a} -> {b} -> {c} -> {d} -> a -> b -> c -> d -> Tuple4 a b c d
-testdata/Internals.lc 18:30-18:31  Type
-testdata/Internals.lc 18:32-18:33  Type
-testdata/Internals.lc 18:34-18:35  Type
-testdata/Internals.lc 18:36-18:37  Type
-testdata/Internals.lc 19:6-19:12  Type | Type -> Type -> Type -> Type -> Type->Type
-testdata/Internals.lc 19:6-19:31  Type
-testdata/Internals.lc 19:6-19:41  Type
-testdata/Internals.lc 19:25-19:31  Tuple5 V10 V9 V8 V7 V6 | Type | {a} -> {b} -> {c} -> {d} -> {e} -> a -> b -> c -> d -> e -> Tuple5 a b c d e
-testdata/Internals.lc 19:32-19:33  Type
-testdata/Internals.lc 19:34-19:35  Type
-testdata/Internals.lc 19:36-19:37  Type
-testdata/Internals.lc 19:38-19:39  Type
-testdata/Internals.lc 19:40-19:41  Type
-testdata/Internals.lc 25:1-25:8  a:Type -> a -> a->a
-testdata/Internals.lc 25:24-25:25  V1
-testdata/Internals.lc 25:24-25:35  Type
-testdata/Internals.lc 25:29-25:30  Type
-testdata/Internals.lc 25:29-25:35  Type
-testdata/Internals.lc 25:34-25:35  Type
-testdata/Internals.lc 27:13-27:17  a:Type -> a -> a->Type
-testdata/Internals.lc 27:24-27:28  Type
-testdata/Internals.lc 27:36-27:37  Type
-testdata/Internals.lc 27:36-27:46  Type
-testdata/Internals.lc 27:45-27:46  Type
-testdata/Internals.lc 28:13-28:15  Type -> Type->Type
-testdata/Internals.lc 31:1-31:4  Unit -> Unit->Unit
-testdata/Internals.lc 31:8-31:12  Type
-testdata/Internals.lc 31:16-31:20  Type
-testdata/Internals.lc 31:16-31:28  Type
-testdata/Internals.lc 31:24-31:28  Type
-testdata/Internals.lc 34:6-34:9  Type
-testdata/Internals.lc 35:6-35:10  Type
-testdata/Internals.lc 36:6-36:11  Type
-testdata/Internals.lc 37:6-37:10  Type
-testdata/Internals.lc 39:6-39:10  Type
-testdata/Internals.lc 39:6-39:25  Type
-testdata/Internals.lc 39:13-39:18  Bool
-testdata/Internals.lc 39:21-39:25  Bool
-testdata/Internals.lc 41:6-41:14  Type
-testdata/Internals.lc 41:6-41:29  Type
-testdata/Internals.lc 41:17-41:19  Ordering
-testdata/Internals.lc 41:22-41:24  Ordering
-testdata/Internals.lc 41:27-41:29  Ordering
-testdata/Internals.lc 44:1-44:14  Int->Word
-testdata/Internals.lc 44:24-44:27  Type
-testdata/Internals.lc 44:33-44:37  Type
-testdata/Internals.lc 45:1-45:15  Int->Float
-testdata/Internals.lc 45:24-45:27  Type
-testdata/Internals.lc 45:33-45:38  Type
-testdata/Internals.lc 46:1-46:15  Int -> Int->Ordering
-testdata/Internals.lc 46:24-46:27  Type
-testdata/Internals.lc 46:33-46:36  Type
-testdata/Internals.lc 46:33-46:50  Type
-testdata/Internals.lc 46:42-46:50  Type
-testdata/Internals.lc 47:1-47:16  Word -> Word->Ordering
-testdata/Internals.lc 47:24-47:28  Type
+testdata/Internals.lc 6:1-6:8  {a} -> a->a
+testdata/Internals.lc 6:13-6:14  V1
+testdata/Internals.lc 8:1-8:10  {a}->a
+testdata/Internals.lc 8:27-8:31  Type
+testdata/Internals.lc 8:35-8:36  Type
+testdata/Internals.lc 10:1-10:8  {a} -> a->a -> a
+testdata/Internals.lc 10:25-10:29  Type
+testdata/Internals.lc 10:33-10:46  Type
+testdata/Internals.lc 10:34-10:35  Type
+testdata/Internals.lc 10:39-10:40  Type
+testdata/Internals.lc 10:45-10:46  Type
+testdata/Internals.lc 12:6-12:10  Type
+testdata/Internals.lc 12:6-12:15  Type
+testdata/Internals.lc 12:13-12:15  Unit
+testdata/Internals.lc 13:6-13:12  Type
+testdata/Internals.lc 14:6-14:11  String->Type | Type
+testdata/Internals.lc 14:18-14:24  Type
+testdata/Internals.lc 17:6-17:12  Type
+testdata/Internals.lc 17:6-17:21  Type
+testdata/Internals.lc 17:15-17:21  Tuple0
+testdata/Internals.lc 18:6-18:12  Type | Type->Type
+testdata/Internals.lc 18:6-18:23  Type
+testdata/Internals.lc 18:6-18:25  Type
+testdata/Internals.lc 18:17-18:23  Tuple1 V2 | Type | {a} -> a -> Tuple1 a
+testdata/Internals.lc 18:24-18:25  Type
+testdata/Internals.lc 19:6-19:12  Type | Type -> Type->Type
+testdata/Internals.lc 19:6-19:25  Type
+testdata/Internals.lc 19:6-19:29  Type
+testdata/Internals.lc 19:19-19:25  Tuple2 V4 V3 | Type | {a} -> {b} -> a -> b -> Tuple2 a b
+testdata/Internals.lc 19:26-19:27  Type
+testdata/Internals.lc 19:28-19:29  Type
+testdata/Internals.lc 20:6-20:12  Type | Type -> Type -> Type->Type
+testdata/Internals.lc 20:6-20:27  Type
+testdata/Internals.lc 20:6-20:33  Type
+testdata/Internals.lc 20:21-20:27  Tuple3 V6 V5 V4 | Type | {a} -> {b} -> {c} -> a -> b -> c -> Tuple3 a b c
+testdata/Internals.lc 20:28-20:29  Type
+testdata/Internals.lc 20:30-20:31  Type
+testdata/Internals.lc 20:32-20:33  Type
+testdata/Internals.lc 21:6-21:12  Type | Type -> Type -> Type -> Type->Type
+testdata/Internals.lc 21:6-21:29  Type
+testdata/Internals.lc 21:6-21:37  Type
+testdata/Internals.lc 21:23-21:29  Tuple4 V8 V7 V6 V5 | Type | {a} -> {b} -> {c} -> {d} -> a -> b -> c -> d -> Tuple4 a b c d
+testdata/Internals.lc 21:30-21:31  Type
+testdata/Internals.lc 21:32-21:33  Type
+testdata/Internals.lc 21:34-21:35  Type
+testdata/Internals.lc 21:36-21:37  Type
+testdata/Internals.lc 22:6-22:12  Type | Type -> Type -> Type -> Type -> Type->Type
+testdata/Internals.lc 22:6-22:31  Type
+testdata/Internals.lc 22:6-22:41  Type
+testdata/Internals.lc 22:25-22:31  Tuple5 V10 V9 V8 V7 V6 | Type | {a} -> {b} -> {c} -> {d} -> {e} -> a -> b -> c -> d -> e -> Tuple5 a b c d e
+testdata/Internals.lc 22:32-22:33  Type
+testdata/Internals.lc 22:34-22:35  Type
+testdata/Internals.lc 22:36-22:37  Type
+testdata/Internals.lc 22:38-22:39  Type
+testdata/Internals.lc 22:40-22:41  Type
+testdata/Internals.lc 28:1-28:8  a:Type -> a -> a->a
+testdata/Internals.lc 28:24-28:25  V1
+testdata/Internals.lc 28:24-28:35  Type
+testdata/Internals.lc 28:29-28:30  Type
+testdata/Internals.lc 28:29-28:35  Type
+testdata/Internals.lc 28:34-28:35  Type
+testdata/Internals.lc 30:13-30:17  a:Type -> a -> a->Type
+testdata/Internals.lc 30:24-30:28  Type
+testdata/Internals.lc 30:36-30:37  Type
+testdata/Internals.lc 30:36-30:46  Type
+testdata/Internals.lc 30:45-30:46  Type
+testdata/Internals.lc 31:13-31:15  Type -> Type->Type
+testdata/Internals.lc 34:1-34:4  Unit -> Unit->Unit
+testdata/Internals.lc 34:8-34:12  Type
+testdata/Internals.lc 34:16-34:20  Type
+testdata/Internals.lc 34:16-34:28  Type
+testdata/Internals.lc 34:24-34:28  Type
+testdata/Internals.lc 37:6-37:9  Type
+testdata/Internals.lc 38:6-38:10  Type
+testdata/Internals.lc 39:6-39:11  Type
+testdata/Internals.lc 40:6-40:10  Type
+testdata/Internals.lc 42:6-42:10  Type
+testdata/Internals.lc 42:6-42:25  Type
+testdata/Internals.lc 42:13-42:18  Bool
+testdata/Internals.lc 42:21-42:25  Bool
+testdata/Internals.lc 44:6-44:14  Type
+testdata/Internals.lc 44:6-44:29  Type
+testdata/Internals.lc 44:17-44:19  Ordering
+testdata/Internals.lc 44:22-44:24  Ordering
+testdata/Internals.lc 44:27-44:29  Ordering
+testdata/Internals.lc 47:1-47:14  Int->Word
+testdata/Internals.lc 47:24-47:27  Type
 testdata/Internals.lc 47:33-47:37  Type
-testdata/Internals.lc 47:33-47:50  Type
-testdata/Internals.lc 47:42-47:50  Type
-testdata/Internals.lc 48:1-48:17  Float -> Float->Ordering
-testdata/Internals.lc 48:24-48:29  Type
+testdata/Internals.lc 48:1-48:15  Int->Float
+testdata/Internals.lc 48:24-48:27  Type
 testdata/Internals.lc 48:33-48:38  Type
-testdata/Internals.lc 48:33-48:50  Type
-testdata/Internals.lc 48:42-48:50  Type
-testdata/Internals.lc 49:1-49:16  Char -> Char->Ordering
-testdata/Internals.lc 49:24-49:28  Type
-testdata/Internals.lc 49:33-49:37  Type
+testdata/Internals.lc 49:1-49:15  Int -> Int->Ordering
+testdata/Internals.lc 49:24-49:27  Type
+testdata/Internals.lc 49:33-49:36  Type
 testdata/Internals.lc 49:33-49:50  Type
 testdata/Internals.lc 49:42-49:50  Type
-testdata/Internals.lc 50:1-50:18  String -> String->Ordering
-testdata/Internals.lc 50:24-50:30  Type
-testdata/Internals.lc 50:34-50:40  Type
-testdata/Internals.lc 50:34-50:52  Type
-testdata/Internals.lc 50:44-50:52  Type
-testdata/Internals.lc 51:1-51:14  Int->Int
-testdata/Internals.lc 51:24-51:27  Type
-testdata/Internals.lc 51:33-51:36  Type
-testdata/Internals.lc 52:1-52:15  Word->Word
+testdata/Internals.lc 50:1-50:16  Word -> Word->Ordering
+testdata/Internals.lc 50:24-50:28  Type
+testdata/Internals.lc 50:33-50:37  Type
+testdata/Internals.lc 50:33-50:50  Type
+testdata/Internals.lc 50:42-50:50  Type
+testdata/Internals.lc 51:1-51:17  Float -> Float->Ordering
+testdata/Internals.lc 51:24-51:29  Type
+testdata/Internals.lc 51:33-51:38  Type
+testdata/Internals.lc 51:33-51:50  Type
+testdata/Internals.lc 51:42-51:50  Type
+testdata/Internals.lc 52:1-52:16  Char -> Char->Ordering
 testdata/Internals.lc 52:24-52:28  Type
 testdata/Internals.lc 52:33-52:37  Type
-testdata/Internals.lc 53:1-53:16  Float->Float
-testdata/Internals.lc 53:24-53:29  Type
-testdata/Internals.lc 53:33-53:38  Type
-testdata/Internals.lc 54:1-54:11  Int -> Int->Int
+testdata/Internals.lc 52:33-52:50  Type
+testdata/Internals.lc 52:42-52:50  Type
+testdata/Internals.lc 53:1-53:18  String -> String->Ordering
+testdata/Internals.lc 53:24-53:30  Type
+testdata/Internals.lc 53:34-53:40  Type
+testdata/Internals.lc 53:34-53:52  Type
+testdata/Internals.lc 53:44-53:52  Type
+testdata/Internals.lc 54:1-54:14  Int->Int
 testdata/Internals.lc 54:24-54:27  Type
 testdata/Internals.lc 54:33-54:36  Type
-testdata/Internals.lc 54:33-54:45  Type
-testdata/Internals.lc 54:42-54:45  Type
-testdata/Internals.lc 55:1-55:11  Int -> Int->Int
-testdata/Internals.lc 55:24-55:27  Type
-testdata/Internals.lc 55:33-55:36  Type
-testdata/Internals.lc 55:33-55:45  Type
-testdata/Internals.lc 55:42-55:45  Type
-testdata/Internals.lc 56:1-56:11  Int -> Int->Int
-testdata/Internals.lc 56:24-56:27  Type
-testdata/Internals.lc 56:33-56:36  Type
-testdata/Internals.lc 56:33-56:45  Type
-testdata/Internals.lc 56:42-56:45  Type
-testdata/Internals.lc 57:1-57:14  Float->Float
-testdata/Internals.lc 57:24-57:29  Type
-testdata/Internals.lc 57:33-57:38  Type
-testdata/Internals.lc 58:1-58:10  Float->Int
-testdata/Internals.lc 58:24-58:29  Type
+testdata/Internals.lc 55:1-55:15  Word->Word
+testdata/Internals.lc 55:24-55:28  Type
+testdata/Internals.lc 55:33-55:37  Type
+testdata/Internals.lc 56:1-56:16  Float->Float
+testdata/Internals.lc 56:24-56:29  Type
+testdata/Internals.lc 56:33-56:38  Type
+testdata/Internals.lc 57:1-57:11  Int -> Int->Int
+testdata/Internals.lc 57:24-57:27  Type
+testdata/Internals.lc 57:33-57:36  Type
+testdata/Internals.lc 57:33-57:45  Type
+testdata/Internals.lc 57:42-57:45  Type
+testdata/Internals.lc 58:1-58:11  Int -> Int->Int
+testdata/Internals.lc 58:24-58:27  Type
 testdata/Internals.lc 58:33-58:36  Type
-testdata/Internals.lc 61:19-61:23  Type
-testdata/Internals.lc 61:19-61:38  Type
-testdata/Internals.lc 61:27-61:28  V2
-testdata/Internals.lc 61:27-61:38  Type
-testdata/Internals.lc 61:32-61:33  Type
-testdata/Internals.lc 61:32-61:38  Type
-testdata/Internals.lc 61:37-61:38  Type
-testdata/Internals.lc 62:1-62:15  {a} -> Bool -> a -> a->a
-testdata/Internals.lc 62:16-62:20  Bool
-testdata/Internals.lc 62:16-63:29  Bool -> V1 -> V2->V3 | V1 -> V2->V3 | V2->V3 | V3
-testdata/Internals.lc 62:28-62:29  V3
-testdata/Internals.lc 62:28-63:29  Bool->V4
-testdata/Internals.lc 63:28-63:29  V4
-testdata/Internals.lc 66:7-66:10  Type->Type
-testdata/Internals.lc 66:7-67:22  Type
-testdata/Internals.lc 66:7-68:32  Type
-testdata/Internals.lc 66:7-69:19  Type
-testdata/Internals.lc 67:3-67:10  {a} -> {b : Num a} -> Int->a
-testdata/Internals.lc 67:14-67:17  Type
-testdata/Internals.lc 67:14-67:22  Type
-testdata/Internals.lc 67:21-67:22  Type
-testdata/Internals.lc 68:3-68:10  {a} -> {b : Num a} -> a -> a->Ordering
-testdata/Internals.lc 68:14-68:15  Type
-testdata/Internals.lc 68:14-68:32  Type
-testdata/Internals.lc 68:19-68:20  Type
-testdata/Internals.lc 68:19-68:32  Type
-testdata/Internals.lc 68:24-68:32  Type
-testdata/Internals.lc 69:3-69:9  {a} -> {b : Num a} -> a->a
-testdata/Internals.lc 69:13-69:14  Type
-testdata/Internals.lc 69:13-69:19  Type
-testdata/Internals.lc 69:18-69:19  Type
-testdata/Internals.lc 71:14-71:17  Type
-testdata/Internals.lc 71:14-72:20  ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
-testdata/Internals.lc 71:14-73:27  ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
-testdata/Internals.lc 71:14-74:26  ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
-testdata/Internals.lc 71:14-79:19  Type | Type->Type
-testdata/Internals.lc 71:14-80:27  {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a
-testdata/Internals.lc 71:14-81:29  {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering
-testdata/Internals.lc 71:14-82:28  {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a
-testdata/Internals.lc 72:13-72:20  Int->Int
-testdata/Internals.lc 72:19-72:20  Int
-testdata/Internals.lc 73:13-73:27  Int -> Int->Ordering
-testdata/Internals.lc 74:13-74:26  Int->Int
-testdata/Internals.lc 75:14-75:18  Type
-testdata/Internals.lc 75:14-76:26  ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
-testdata/Internals.lc 75:14-77:28  ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
-testdata/Internals.lc 75:14-78:27  ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
-testdata/Internals.lc 75:14-79:19  Type
-testdata/Internals.lc 75:14-80:27  {a : Num V0} -> Int->V2
-testdata/Internals.lc 75:14-81:29  {a : Num V0} -> V1 -> V2->Ordering
-testdata/Internals.lc 75:14-82:28  {a : Num V0} -> V1->V2
-testdata/Internals.lc 76:13-76:26  Int->Word
-testdata/Internals.lc 77:13-77:28  Word -> Word->Ordering
-testdata/Internals.lc 78:13-78:27  Word->Word
-testdata/Internals.lc 79:14-79:19  Type
-testdata/Internals.lc 79:14-80:27  ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
-testdata/Internals.lc 79:14-81:29  ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
-testdata/Internals.lc 79:14-82:28  ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
-testdata/Internals.lc 80:13-80:27  Int->Float
-testdata/Internals.lc 81:13-81:29  Float -> Float->Ordering
-testdata/Internals.lc 82:13-82:28  Float->Float
+testdata/Internals.lc 58:33-58:45  Type
+testdata/Internals.lc 58:42-58:45  Type
+testdata/Internals.lc 59:1-59:11  Int -> Int->Int
+testdata/Internals.lc 59:24-59:27  Type
+testdata/Internals.lc 59:33-59:36  Type
+testdata/Internals.lc 59:33-59:45  Type
+testdata/Internals.lc 59:42-59:45  Type
+testdata/Internals.lc 60:1-60:14  Float->Float
+testdata/Internals.lc 60:24-60:29  Type
+testdata/Internals.lc 60:33-60:38  Type
+testdata/Internals.lc 61:1-61:10  Float->Int
+testdata/Internals.lc 61:24-61:29  Type
+testdata/Internals.lc 61:33-61:36  Type
+testdata/Internals.lc 64:19-64:23  Type
+testdata/Internals.lc 64:19-64:38  Type
+testdata/Internals.lc 64:27-64:28  V2
+testdata/Internals.lc 64:27-64:38  Type
+testdata/Internals.lc 64:32-64:33  Type
+testdata/Internals.lc 64:32-64:38  Type
+testdata/Internals.lc 64:37-64:38  Type
+testdata/Internals.lc 65:1-65:15  {a} -> Bool -> a -> a->a
+testdata/Internals.lc 65:16-65:20  Bool
+testdata/Internals.lc 65:16-66:29  Bool -> V1 -> V2->V3 | V1 -> V2->V3 | V2->V3 | V3
+testdata/Internals.lc 65:28-65:29  V3
+testdata/Internals.lc 65:28-66:29  Bool->V4
+testdata/Internals.lc 66:28-66:29  V4
+testdata/Internals.lc 69:7-69:10  Type->Type
+testdata/Internals.lc 69:7-70:22  Type
+testdata/Internals.lc 69:7-71:32  Type
+testdata/Internals.lc 69:7-72:19  Type
+testdata/Internals.lc 70:3-70:10  {a} -> {b : Num a} -> Int->a
+testdata/Internals.lc 70:14-70:17  Type
+testdata/Internals.lc 70:14-70:22  Type
+testdata/Internals.lc 70:21-70:22  Type
+testdata/Internals.lc 71:3-71:10  {a} -> {b : Num a} -> a -> a->Ordering
+testdata/Internals.lc 71:14-71:15  Type
+testdata/Internals.lc 71:14-71:32  Type
+testdata/Internals.lc 71:19-71:20  Type
+testdata/Internals.lc 71:19-71:32  Type
+testdata/Internals.lc 71:24-71:32  Type
+testdata/Internals.lc 72:3-72:9  {a} -> {b : Num a} -> a->a
+testdata/Internals.lc 72:13-72:14  Type
+testdata/Internals.lc 72:13-72:19  Type
+testdata/Internals.lc 72:18-72:19  Type
+testdata/Internals.lc 74:14-74:17  Type
+testdata/Internals.lc 74:14-75:20  ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
+testdata/Internals.lc 74:14-76:27  ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
+testdata/Internals.lc 74:14-77:26  ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
+testdata/Internals.lc 74:14-82:19  Type | Type->Type
+testdata/Internals.lc 74:14-83:27  {a : Num V0} -> Int->V2 | {a} -> {b : Num a} -> Int->a
+testdata/Internals.lc 74:14-84:29  {a : Num V0} -> V1 -> V2->Ordering | {a} -> {b : Num a} -> a -> a->Ordering
+testdata/Internals.lc 74:14-85:28  {a : Num V0} -> V1->V2 | {a} -> {b : Num a} -> a->a
+testdata/Internals.lc 75:13-75:20  Int->Int
+testdata/Internals.lc 75:19-75:20  Int
+testdata/Internals.lc 76:13-76:27  Int -> Int->Ordering
+testdata/Internals.lc 77:13-77:26  Int->Int
+testdata/Internals.lc 78:14-78:18  Type
+testdata/Internals.lc 78:14-79:26  ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
+testdata/Internals.lc 78:14-80:28  ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
+testdata/Internals.lc 78:14-81:27  ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
+testdata/Internals.lc 78:14-82:19  Type
+testdata/Internals.lc 78:14-83:27  {a : Num V0} -> Int->V2
+testdata/Internals.lc 78:14-84:29  {a : Num V0} -> V1 -> V2->Ordering
+testdata/Internals.lc 78:14-85:28  {a : Num V0} -> V1->V2
+testdata/Internals.lc 79:13-79:26  Int->Word
+testdata/Internals.lc 80:13-80:28  Word -> Word->Ordering
+testdata/Internals.lc 81:13-81:27  Word->Word
+testdata/Internals.lc 82:14-82:19  Type
+testdata/Internals.lc 82:14-83:27  ({a : Num V0} -> Int->V2) -> {d : Num V1} -> Int->V3
+testdata/Internals.lc 82:14-84:29  ({a : Num V0} -> V1 -> V2->Ordering) -> {e : Num V1} -> V2 -> V3->Ordering
+testdata/Internals.lc 82:14-85:28  ({a : Num V0} -> V1->V2) -> {d : Num V1} -> V2->V3
+testdata/Internals.lc 83:13-83:27  Int->Float
+testdata/Internals.lc 84:13-84:29  Float -> Float->Ordering
+testdata/Internals.lc 85:13-85:28  Float->Float