11 files changed, 407 insertions, 154 deletions

diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 7e6bc883..405bb06a 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -69,7 +69,7 @@ data Stmt
     = Let SIName MFixity (Maybe SExp) [Visibility]{-source arity-} SExp
     | Data SIName [(Visibility, SExp)]{-parameters-} SExp{-type-} Bool{-True:add foralls-} [(SIName, SExp)]{-constructor names and types-}
     | PrecDef SIName Fixity
-    | ValueDef ([SName], Pat) SExp
+    | ValueDef ([SIName], Pat) SExp
     | TypeFamily SIName [(Visibility, SExp)]{-parameters-} SExp{-type-}
 
     -- eliminated during parsing
@@ -1156,8 +1156,8 @@ getParams x = ([], x)
 getLams (Lam h a b) = ((h, a):) *** id $ getLams b
 getLams x = ([], x)
 
-apps a b = foldl SAppV{-SI todo-} (SGlobal ((debugSI "8"){-todo-}, a)) b
-apps' a b = foldl sapp{-SI todo-} (SGlobal ((debugSI "9"){-todo-}, a)) b
+apps a b = foldl SAppV{-SI todo-} (SGlobal a) b
+apps' a b = foldl sapp{-SI todo-} (SGlobal a) b
 
 replaceMetas err bind = \case
     Meta a t -> bind Hidden a <$> replaceMetas err bind t
@@ -1331,14 +1331,14 @@ handleStmt exs = \case
                 addToEnv exs (si, cn) (Con conn [], cty)
                 return ( conn
                        , addParamsS pars
-                       $ foldl SAppV (SVar (debugSI "22", ".cs") $ j + length pars) $ drop pnum' xs ++ [apps' cn (zip acts $ downToS (j+1+length pars) (length ps) ++ downToS 0 (act- length ps))]
+                       $ foldl SAppV (SVar (debugSI "22", ".cs") $ j + length pars) $ drop pnum' xs ++ [apps' (si, cn) (zip acts $ downToS (j+1+length pars) (length ps) ++ downToS 0 (act- length ps))]
                        )
             | otherwise = throwError $ "illegal data definition (parameters are not uniform) " -- ++ show (c, cn, take pnum' xs, act)
             where
                 (c, map snd -> xs) = getApps $ snd $ getParamsS ct
 
         motive = addParamsS (replicate inum (Visible, Wildcard SType)) $
-           SPi Visible (apps' s $ zip (map fst ps) (downToS inum $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS 0 inum)) SType
+           SPi Visible (apps' (si, s) $ zip (map fst ps) (downToS inum $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS 0 inum)) SType
 
     mdo
         let tcn = TyConName s Nothing inum vty (map fst cons) ct
@@ -1350,7 +1350,7 @@ handleStmt exs = \case
                 ++ (Visible, motive)
                 : map ((,) Visible . snd) cons
                 ++ replicate inum (Hidden, Wildcard SType)
-                ++ [(Visible, apps' s $ zip (map fst ps) (downToS (inum + length cs + 1) $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS 0 inum))]
+                ++ [(Visible, apps' (si, s) $ zip (map fst ps) (downToS (inum + length cs + 1) $ length ps) ++ zip (map fst $ fst $ getParamsS t_) (downToS 0 inum))]
                 )
             $ foldl SAppV (SVar (debugSI "23", ".ct") $ length cs + inum + 1) $ downToS 1 inum ++ [SVar (debugSI "24", ".24") 0]
             )
@@ -1513,7 +1513,7 @@ fixityDef = do
         <|> InfixR <$ reserved "infixr"
   localIndentation Gt $ do
     i <- fromIntegral <$> natural
-    ns <- commaSep1 (siName operatorT)
+    ns <- commaSep1 (withSI operatorT)
     return $ PrecDef <$> ns <*> pure (dir, i)
 
 -------------------------------------------------------------------------------- export
@@ -1615,44 +1615,54 @@ parseLC f str = either (throwError . ErrorMsg . show) return . flip runReader (e
 
 --------------------------------------------------------------------------------
 
-parseType ns mb vs = maybe id option mb $ reservedOp "::" *> (dbf' vs <$> parseTTerm ns PrecLam)
-typedIds ns mb vs = (,) <$> commaSep1 (siName (varId ns <|> patVar ns <|> upperCase ns))
-                        <*> localIndentation Gt {-TODO-} (parseType ns mb vs)
-
-telescope ns mb = (removeSI *** id) <$> telescopeSI ns mb []
-
-telescopeSI :: Namespace -> Maybe SExp -> [SIName] -> P ([SIName], [(Visibility, SExp)])    -- todo: refactor to [(SIName, (Visibility, SExp))]
-telescopeSI ns mb vs = option (vs, []) $ do
-    (si, (x, vt)) <- withSI
-      (     reservedOp "@" *> (maybe empty (\x -> flip (,) (Hidden, x) <$> patVar ns) mb <|> parens (typedId Hidden))
-        <|> try (parens $ typedId Visible)
-        <|> maybe ((,) "" . (,) Visible . dbf' (removeSI vs) <$> parseTerm ns PrecAtom)
-                  (\x -> flip (,) (Visible, x) <$> patVar ns)
-                  mb
-      )
-    (second (vt:)) <$> telescopeSI ns mb ((si, x): vs)
-  where
-    typedId v = (\f s -> (f,(v,s)))
-                  <$> patVar ns
-                  <*> localIndentation Gt {-TODO-} (parseType ns mb (removeSI vs))
+parseType ns mb = maybe id option mb (reservedOp "::" *> parseTTerm ns PrecLam)
+typedIds ns mb = (,) <$> commaSep1 (withSI (varId ns <|> patVar ns <|> upperCase ns))
+                     <*> localIndentation Gt {-TODO-} (parseType ns mb)
+
+telescope ns mb = (DBNamesC *** id) <$> telescopeSI ns mb
 
-removeSI = DBNamesC . map snd
+telescopeSI :: Namespace -> Maybe SExp -> P ([SIName], [(Visibility, SExp)])    -- todo: refactor to [(SIName, (Visibility, SExp))]
+telescopeSI ns mb = go []
+  where
+    go vs = option ([], []) $ do
+        (x, vt) <-
+          (     reservedOp "@" *> (maybe empty (\x -> flip (,) (Hidden, x) <$> withSI (patVar ns)) mb <|> parens (typedId Hidden))
+            <|> try (parens $ typedId Visible)
+            <|> maybe ((,) (debugSI "s13", "") . (,) Visible . dbf' (DBNamesC vs) <$> parseTerm ns PrecAtom)
+                      (\x -> flip (,) (Visible, x) <$> withSI (patVar ns))
+                      mb
+          )
+        ((++[x]) *** (vt:)) <$> go (x: vs)
+      where
+        typedId v = (\f s -> (f,(v,s)))
+                      <$> withSI (patVar ns)
+                      <*> localIndentation Gt {-TODO-} (dbf' (DBNamesC vs) <$> parseType ns mb)
 
-parseClause ns e = do
-    (fe, p) <- pattern' ns e
+telescopeDataFields :: Namespace -> P ([SIName], [(Visibility, SExp)]) 
+telescopeDataFields ns = {-telescopeSI ns Nothing-} go []
+  where
+    go vs = option ([], []) $ do
+        (x, vt) <- do name <- withSI $ var (expNS ns)
+                      term <- parseType ns Nothing
+                      return (name, (Visible, dbf' (DBNamesC vs) term))
+        ((++[x]) *** (vt:)) <$> (comma *> go (x: vs) <|> pure ([], []))
+
+parseClause ns = do
+    (fe, p) <- pattern' ns
     localIndentation Gt $ do
-        x <- reservedOp "->" *> (dbf' fe <$> parseETerm ns PrecLam)
+        x <- reservedOp "->" *> parseETerm ns PrecLam
         f <- parseWhereBlock ns
         return (p, dbf' fe $ f x)
 
-patternAtom ns vs =
-     (,) vs . flip ViewPat eqPP . SAppV (SGlobal (debugSI "patternAtom1","primCompareFloat")) <$> sLit `withRange` (LFloat <$> try float)
- <|> (,) vs . mkNatPat ns <$> (withSI natural)
- <|> (,) vs . flip PCon [] <$> (siName $ upperCase ns)
- <|> char '\'' *> patternAtom (switchNS ns) vs
- <|> (\sn@(si, n) -> (addDBName n vs, PVar sn)) <$> withSI (patVar ns)
- <|> (id *** (pConSI . mkListPat ns)) <$> brackets (patlist ns vs <|> pure (vs, []))
- <|> (id *** (pConSI . mkTupPat ns)) <$> parens (patlist ns vs)
+patternAtom ns = patternAtom' ns <&> \p -> (getPVars p, p)
+patternAtom' ns =
+     flip ViewPat eqPP . SAppV (SGlobal (debugSI "patternAtom1","primCompareFloat")) <$> sLit `withRange` (LFloat <$> try float)
+ <|> mkNatPat ns <$> (withSI natural)
+ <|> flip PCon [] <$> (withSI $ upperCase ns)
+ <|> char '\'' *> patternAtom' (switchNS ns)
+ <|> PVar <$> withSI (patVar ns)
+ <|> pConSI . mkListPat ns <$> brackets (patlist ns <|> pure [])
+ <|> pConSI . mkTupPat ns <$> parens (patlist ns)
  where
    mkNatPat (Namespace ExpLevel _) (si, n) = flip ViewPat eqPP . SAppV (SGlobal (debugSI "patternAtom2","primCompareInt")) . sLit si . LInt $ fromIntegral n
    mkNatPat _ (si, n) = toNatP si n
@@ -1662,7 +1672,7 @@ patternAtom ns vs =
 eqPP = ParPat [PCon (debugSI "eqPP", "EQ") []]
 truePP = ParPat [PCon (debugSI "truePP", "True") []]
 
-patlist ns vs = commaSepUnfold (\vs -> (\(vs, p) t -> (vs, patType p t)) <$> pattern' ns vs <*> parseType ns (Just $ Wildcard SType) vs) vs
+patlist ns = fmap snd $ commaSepUnfold (\vs -> (\(vs, p) t -> (vs, patType (dbPat vs p) t)) <$> pattern' ns <*> (dbf' vs <$> parseType ns (Just $ Wildcard SType))) mempty
 
 mkListPat ns [p] | namespaceLevel ns == Just TypeLevel = PCon (debugSI "mkListPat4", "'List") [ParPat [p]]
 mkListPat ns (p: ps) = PCon (debugSI "mkListPat2", "Cons") $ map (ParPat . (:[])) [p, mkListPat ns ps]
@@ -1672,37 +1682,42 @@ mkTupPat :: Namespace -> [Pat] -> Pat
 mkTupPat _ [x] = x
 mkTupPat ns ps = PCon (debugSI "", tick' ns $ "Tuple" ++ show (length ps)) (ParPat . (:[]) <$> ps)
 
-pattern' ns vs =
-     pCon <$> (siName $ upperCase ns) <*> patterns ns vs
- <|> pCon <$> try (withSI (char '\'' *> upperCase (switchNS ns))) <*> patterns ns vs
- <|> (patternAtom ns vs >>= \(vs, p) -> option (vs, p) ((id *** (\p' -> PCon (debugSI "pattern'","Cons") (ParPat . (:[]) <$> [p, p']))) <$ reservedOp ":" <*> pattern' ns vs))
+pattern' ns = pattern'_ ns <&> \p -> (getPVars p, p)
+pattern'_ ns =
+     PCon <$> (withSI $ upperCase ns) <*> patterns' ns
+ <|> PCon <$> try (withSI (char '\'' *> upperCase (switchNS ns))) <*> patterns' ns
+ <|> (patternAtom ns >>= \(vs, p) -> option p (((\p' -> PCon (debugSI "pattern'","Cons") (ParPat . (:[]) <$> [p, p']))) <$ reservedOp ":" <*> (dbPat vs <$> pattern'_ ns)))
+
+dbPat v = mapP (dbf' v)
 
 pCon i (vs, x) = (vs, PCon i x)
 
-patterns ns vs =
-     do patternAtom ns vs >>= \(vs, p) -> patterns ns vs >>= \(vs, ps) -> pure (vs, ParPat [p]: ps)
- <|> pure (vs, [])
+patterns ns = patterns' ns <&> \p -> (foldMap getPPVars p, p)
+patterns' ns = fmap snd $
+     do patternAtom ns >>= \(vs, p) -> patterns ns >>= \(vs', ps) -> pure (vs' <> vs, ParPat [p]: map (mapPP $ dbf' vs) ps)
+ <|> pure (mempty, [])
 
 patType p (Wildcard SType) = p
 patType p t = PatType (ParPat [p]) t
 
-commaSepUnfold1 :: (t -> P (t, a)) -> t -> P (t, [a])
-commaSepUnfold1 p vs0 = do
-  (vs1, x) <- p vs0
-  (second (x:) <$ comma <*> commaSepUnfold1 p vs1) <|> pure (vs1, [x])
-
+-- todo: eliminate
 commaSepUnfold :: (t -> P (t, a)) -> t -> P (t, [a])
 commaSepUnfold p vs = commaSepUnfold1 p vs <|> pure (vs, [])
+  where
+    commaSepUnfold1 :: (t -> P (t, a)) -> t -> P (t, [a])
+    commaSepUnfold1 p vs0 = do
+      (vs1, x) <- p vs0
+      (second (x:) <$ comma <*> commaSepUnfold1 p vs1) <|> pure (vs1, [x])
 
 telescope' ns = go mempty where
     go vs = option (vs, []) $ do
         (vs', vt) <-
-                reservedOp "@" *> (f Hidden <$> patternAtom ns vs)
-            <|> f Visible <$> patternAtom ns vs
-        (id *** (vt:)) <$> go vs'
+                reservedOp "@" *> (second (f Hidden . mapP (dbf' vs)) <$> patternAtom ns)
+            <|> second (f Visible . mapP (dbf' vs)) <$> patternAtom ns
+        (id *** (vt:)) <$> go (vs' <> vs)
       where
-        f h (vs, PatType (ParPat [p]) t) = (vs, ((h, t), p))
-        f h (vs, p) = (vs, ((h, Wildcard SType), p))
+        f h (PatType (ParPat [p]) t) = ((h, t), p)
+        f h p = ((h, Wildcard SType), p)
 
 parseDefs lend ns = (asks $ \ge -> compileFunAlts' lend ge . concat) <*> many (parseDef ns)
 
@@ -1756,49 +1771,48 @@ parseDef :: Namespace -> P [Stmt]
 parseDef ns =
      do reserved "data"
         localIndentation Gt $ do
-            (si,x) <- siName $ upperCase (typeNS ns)
-            (nps, ts) <- telescopeSI (typeNS ns) (Just SType) []
-            let npsd@(DBNamesC npsd_) = removeSI nps
-            t <- parseType (typeNS ns) (Just SType) npsd
+            (si,x) <- withSI $ upperCase (typeNS ns)
+            (npsd, ts) <- telescope (typeNS ns) (Just SType)
+            t <- dbf' npsd <$> parseType (typeNS ns) (Just SType)
             let mkConTy mk (nps', ts') =
-                    ( if mk then Just $ diffDBNames' nps' npsd_ else Nothing
+                    ( if mk then Just nps' else Nothing
                     , foldr (uncurry SPi) (foldl SAppV (SGlobal (si,x)) $ downToS (length ts') $ length ts) ts')
             (af, cs) <-
                  do (,) True <$ reserved "where" <*> localIndentation Ge (localAbsoluteIndentation $ many $
-                        (id *** (,) Nothing) <$> typedIds ns Nothing npsd)
+                        (id *** (,) Nothing . dbf' npsd) <$> typedIds ns Nothing)
              <|> do (,) False <$ reservedOp "=" <*>
-                      sepBy1 ((,) <$> (pure <$> siName (upperCase ns))
-                                  <*> (    braces (mkConTy True <$> (telescopeDataFields (typeNS ns) nps))
-                                       <|> (mkConTy False <$> telescopeSI (typeNS ns) Nothing nps)) )
+                      sepBy1 ((,) <$> (pure <$> withSI (upperCase ns))
+                                  <*> (    braces (mkConTy True . (\(x, y) -> (x, zipWith (\i (v, e) -> (v, dbf_ i npsd e)) [0..] y)) <$> telescopeDataFields (typeNS ns))
+                                       <|> (mkConTy False . (\(x, y) -> (x, zipWith (\i (v, e) -> (v, dbf_ i npsd e)) [0..] y)) <$> telescopeSI (typeNS ns) Nothing)) )
                                       (reservedOp "|")
              <|> pure (True, [])
             ge <- ask
             return $ mkData ge (si,x) ts t af $ concatMap (\(vs, t) -> (,) <$> vs <*> pure t) $ cs
  <|> do reserved "class"
         localIndentation Gt $ do
-            x <- siName $ upperCase (typeNS ns)
+            x <- withSI $ upperCase (typeNS ns)
             (nps, ts) <- telescope (typeNS ns) (Just SType)
             cs <-
-                 do reserved "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ typedIds ns Nothing nps)
+                 do reserved "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ typedIds ns Nothing)
              <|> pure []
-            return $ pure $ Class x (map snd ts) (concatMap (\(vs, t) -> (,) <$> vs <*> pure t) cs)
+            return $ pure $ Class x (map snd ts) (concatMap (\(vs, t) -> (,) <$> vs <*> pure (dbf' nps t)) cs)
  <|> do reserved "instance"
         let ns' = typeNS ns
         localIndentation Gt $ do
             constraints <- option [] $ try $ getTTuple' <$> parseTerm ns' PrecEq <* reservedOp "=>"
-            (si,x) <- siName $ upperCase ns'
+            (si,x) <- withSI $ upperCase ns'
             (nps, args) <- telescope' ns'
             cs <- option [] $ reserved "where" *> localIndentation Ge (localAbsoluteIndentation $ some $
                     dbFunAlt nps <$> funAltDef (varId ns) ns)
              <|> pure []
             ge <- ask
-            return $ pure $ Instance (si,x) ({-todo-}map snd args) (dbf (diffDBNames nps ++ [x]) <$> constraints) $ compileFunAlts' id{-TODO-} ge cs
+            return $ pure $ Instance (si,x) ({-todo-}map snd args) (dbff (diffDBNames nps ++ [x]) <$> constraints) $ compileFunAlts' id{-TODO-} ge cs
  <|> do try (reserved "type" >> reserved "family")
         let ns' = typeNS ns
         localIndentation Gt $ do
-            (si, x) <- siName $ upperCase ns'
+            (si, x) <- withSI $ upperCase ns'
             (nps, ts) <- telescope ns' (Just SType)
-            t <- parseType ns' (Just SType) nps
+            t <- dbf' nps <$> parseType ns' (Just SType)
             option {-open type family-}[TypeFamily (si, x) ts t] $ do
                 cs <- reserved "where" *> localIndentation Ge (localAbsoluteIndentation $ many $
                     funAltDef (upperCase ns' >>= \x' -> guard (x == x') >> return x') ns')
@@ -1808,42 +1822,36 @@ parseDef ns =
  <|> do reserved "type"
         let ns' = typeNS ns
         localIndentation Gt $ do
-            (si, x) <- siName $ upperCase ns'
-            (nps, ts) <- telescopeSI ns' (Just (Wildcard SType)) []
+            (si, x) <- withSI $ upperCase ns'
+            (nps, ts) <- telescopeSI ns' (Just (Wildcard SType))
             reservedOp "="
-            rhs <- dbf' (removeSI nps) <$> parseTerm ns' PrecLam
+            rhs <- dbf' (DBNamesC nps) <$> parseTerm ns' PrecLam
             ge <- ask
-            return $ compileFunAlts False id SLabelEnd ge [{-TypeAnn (si, x) $ addParamsS ts $ SType-}{-todo-}] [FunAlt (si, x) (reverse $ zip (reverse ts) $ map PVar nps) Nothing rhs]
+            return $ compileFunAlts False id SLabelEnd ge
+                [{-TypeAnn (si, x) $ addParamsS ts $ SType-}{-todo-}]
+                [FunAlt (si, x) (reverse $ zip (reverse ts) $ map PVar nps) Nothing rhs]
  <|> do try (reserved "type" >> reserved "instance")
         let ns' = typeNS ns
         pure <$> localIndentation Gt (funAltDef (upperCase ns') ns')
- <|> do (vs, t) <- try $ typedIds ns Nothing mempty
+ <|> do (vs, t) <- try $ typedIds ns Nothing
         return $ TypeAnn <$> vs <*> pure t
  <|> fixityDef
  <|> pure <$> funAltDef (varId ns) ns
  <|> pure . uncurry ValueDef <$> valueDef ns
- where
-   telescopeDataFields :: Namespace -> [SIName] -> P ([SIName], [(Visibility, SExp)]) 
-   telescopeDataFields ns vs = option (vs, []) $ do
-       (x, vt) <- do name <- siName $ var (expNS ns)
-                     reservedOp "::"
-                     term <- dbf' (removeSI vs) <$> parseTerm ns PrecLam
-                     return (name, (Visible, term))
-       (id *** (vt:)) <$> (comma *> telescopeDataFields ns (x: vs) <|> pure (vs, []))
 
 funAltDef parseName ns = do   -- todo: use ns to determine parseName
     (n, (fee, tss)) <-
         do try' "operator definition" $ do
-            (e', a1) <- patternAtom ns mempty
+            (e', a1) <- patternAtom ns
             localIndentation Gt $ do
-                n <- siName operatorT
-                (e'', a2) <- patternAtom ns e'
+                n <- withSI operatorT
+                (e'', a2) <- patternAtom ns
                 lookAhead $ reservedOp "=" <|> reservedOp "|"
-                return (n, (e'', (,) (Visible, Wildcard SType) <$> [a1, a2]))
+                return (n, (e'' <> e', (,) (Visible, Wildcard SType) <$> [a1, mapP (dbf' e') a2]))
       <|> do try $ do
-                n <- siName parseName
+                n <- withSI parseName
                 localIndentation Gt $ (,) n <$> telescope' ns <* (lookAhead $ reservedOp "=" <|> reservedOp "|")
-    let fe = addDBNames (diffDBNames fee) $ addDBName (snd n) mempty
+    let fe = dbf' $ fee <> addDBName n
         ts = map (id *** upP 0 1{-todo: replace n with Var 0-}) tss
     localIndentation Gt $ do
         gu <- option Nothing $ do
@@ -1852,7 +1860,7 @@ funAltDef parseName ns = do   -- todo: use ns to determine parseName
         reservedOp "="
         rhs <- parseTerm ns PrecLam
         f <- parseWhereBlock ns
-        return $ FunAlt n ts (dbf' fe <$> gu) $ dbf' fe $ f rhs
+        return $ FunAlt n ts (fe <$> gu) $ fe $ f rhs
 
 dbFunAlt v (FunAlt n ts gu e) = FunAlt n (map (id *** mapP (dbf' v)) ts) (dbf' v <$> gu) $ dbf' v e
 
@@ -1870,19 +1878,19 @@ parseWhereBlock ns = option id $ do
     ge <- ask
     return $ mkLets ge dcls
 
-newtype DBNames = DBNamesC [SName]  -- De Bruijn variable names
-instance Show DBNames where show (DBNamesC x) = show x
+newtype DBNames = DBNamesC [SIName]  -- De Bruijn variable names
+instance Show DBNames where show (DBNamesC x) = show $ map snd x
 instance Monoid DBNames where mempty = DBNamesC []
-                              mappend = error "mappend @DBNames"
+                              mappend (DBNamesC a) (DBNamesC b) = DBNamesC (a ++ b)
+
+addDBName n = DBNamesC [n]
+diffDBNames (DBNamesC xs) = map snd xs
 
-addDBNames xs (DBNamesC ys) = DBNamesC $ xs ++ ys
-addDBName n (DBNamesC ns) = DBNamesC $ n:ns
 sVar = withRange $ \si x -> SGlobal (si, x)
-diffDBNames (DBNamesC xs) = xs
 
-valueDef :: Namespace -> P (([SName], Pat), SExp)
+valueDef :: Namespace -> P (([SIName], Pat), SExp)
 valueDef ns = do
-    (DBNamesC e', p) <- try $ pattern' ns mempty <* reservedOp "="
+    (DBNamesC e', p) <- try $ pattern' ns <* reservedOp "="
     localIndentation Gt $ do
         ex <- parseETerm ns PrecLam
         return ((e', p), ex)
@@ -1907,12 +1915,12 @@ parseTerm ns PrecLam =
             t' <- dbf' fe <$> parseTerm ns PrecLam
             return $ \r -> foldr (uncurry (f r)) t' ts
  <|> do (asks compileCase) <* reserved "case" <*> parseETerm ns PrecLam
-                                 <* reserved "of" <*> localIndentation Ge (localAbsoluteIndentation $ some $ parseClause ns mempty)
+                           <* reserved "of" <*> localIndentation Ge (localAbsoluteIndentation $ some $ parseClause ns)
  <|> do (asks $ \ge -> compileGuardTree id id ge . Alts) <*> parseSomeGuards ns (const True)
  <|> do t <- parseTerm ns PrecEq
         option t $ mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> parseTTerm ns PrecLam
 parseTerm ns PrecEq = parseTerm ns PrecAnn >>= \t -> option t $ SCstr t <$ reservedOp "~" <*> parseTTerm ns PrecAnn
-parseTerm ns PrecAnn = parseTerm ns PrecOp >>= \t -> option t $ SAnn t <$> parseType ns Nothing mempty
+parseTerm ns PrecAnn = parseTerm ns PrecOp >>= \t -> option t $ SAnn t <$> parseType ns Nothing
 parseTerm ns PrecOp = asks calculatePrecs <*> p' where
     p' = ((\si (t, xs) -> (mkNat ns si 0, (SGlobal (debugSI "12", "-"), t): xs)) `withRange` (reservedOp "-" *> p_))
          <|> p_
@@ -1944,8 +1952,8 @@ parseTerm ns PrecAtom =
  <|> mkDotDot <$> try (reservedOp "[" *> parseTerm ns PrecLam <* reservedOp ".." ) <*> parseTerm ns PrecLam <* reservedOp "]"
  <|> listCompr ns
  <|> mkList ns `withRange` brackets (commaSep $ parseTerm ns PrecLam)
- <|> mkLeftSection `withRange` try{-todo: better try-} (parens $ (,) <$> siName (guardM (/= "-") operatorT) <*> parseTerm ns PrecLam)
- <|> mkRightSection `withRange` try{-todo: better try!-} (parens $ (,) <$> parseTerm ns PrecApp <*> siName operatorT)
+ <|> mkLeftSection `withRange` try{-todo: better try-} (parens $ (,) <$> withSI (guardM (/= "-") operatorT) <*> parseTerm ns PrecLam)
+ <|> mkRightSection `withRange` try{-todo: better try!-} (parens $ (,) <$> parseTerm ns PrecApp <*> withSI operatorT)
  <|> mkTuple ns `withRange` parens (commaSep $ parseTerm ns PrecLam)
  <|> mkRecord `withRange` braces (commaSep $ ((,) <$> lowerCase ns <* colon <*> parseTerm ns PrecLam))
  <|> do reserved "let"
@@ -2000,9 +2008,6 @@ mkList _ si xs = error "mkList"
 mkNat (Namespace ExpLevel _) si n = SGlobal (noSI,"fromInt") `SAppV` sLit si (LInt $ fromIntegral n)
 mkNat _ _ n = toNat n
 
-siName :: P SName -> P SIName
-siName = withSI
-
 withSI = withRange (,)
 
 mkIf si (b,t,f) = SGlobal (si,"primIfThenElse") `SAppV` b `SAppV` t `SAppV` f
@@ -2020,13 +2025,13 @@ manyNM n m p = do
 
 generator, letdecl, boolExpression :: Namespace -> DBNames -> P (DBNames, SExp -> SExp)
 generator ns dbs = do
-    (dbs', pat) <- try $ pattern' ns dbs <* reservedOp "<-"
+    (dbs', pat) <- try $ pattern' ns <* reservedOp "<-"
     exp <- dbf' dbs <$> parseTerm ns PrecLam
     ge <- ask
-    return $ (,) dbs' $ \e -> application
+    return $ (,) (dbs' <> dbs) $ \e -> application
         [ SGlobal (noSI, "concatMap")
         , SLamV $ compileGuardTree id id ge $ Alts
-            [ compilePatts [(pat, 0)] Nothing $ {-upS $ -} e
+            [ compilePatts [(mapP (dbf' dbs) pat, 0)] Nothing $ {-upS $ -} e
             , GuardLeaf $ SGlobal (noSI, "Nil")
             ]
         , exp
@@ -2041,7 +2046,7 @@ boolExpression ns dbs = do
 application = foldl1 SAppV
 
 listCompr :: Namespace -> P SExp
-listCompr ns = (\e (dbs', fs) -> foldr ($) (dbf (diffDBNames dbs') e) fs)
+listCompr ns = (\e (dbs', fs) -> foldr ($) (dbff (diffDBNames dbs') e) fs)
  <$> try' "List comprehension" ((SGlobal (noSI, "singleton") `SAppV`) <$ reservedOp "[" <*> parseTerm ns PrecLam <* reservedOp "|")
  <*> commaSepUnfold (liftA2 (<|>) (generator ns) $ liftA2 (<|>) (letdecl ns) (boolExpression ns)) mempty <* reservedOp "]"
 
@@ -2049,11 +2054,11 @@ listCompr ns = (\e (dbs', fs) -> foldr ($) (dbf (diffDBNames dbs') e) fs)
 diffDBNames' xs ys = take (length xs - length ys) xs
 
 dbf' = dbf_ 0
-dbf_ j (DBNamesC xs) e = foldl (\e (i, n) -> substSG n (\si -> SVar (si, n) i) e) e $ zip [j..] xs
+dbf_ j (DBNamesC xs) e = foldl (\e (i, (si, n)) -> substSG n (\si -> SVar (si, n) i) e) e $ zip [j..] xs
 
-dbf :: [String] -> SExp -> SExp
-dbf [] e = e
-dbf (n: ns) e = substSG0 n $ dbf ns e
+dbff :: [String] -> SExp -> SExp
+dbff [] e = e
+dbff (n: ns) e = substSG0 n $ dbff ns e
 
 --------------------------------------------------------------------------------
 
@@ -2145,7 +2150,7 @@ mkLets :: GlobalEnv' -> [Stmt]{-where block-} -> SExp{-main expression-} -> SExp
 mkLets _ [] e = e
 mkLets ge (Let n _ mt _ (downS 0 -> Just x): ds) e
     = SLet (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 (snd n) $ mkLets ge ds e)
-mkLets ge (ValueDef (ns, p) x: ds) e = patLam (debugSI "13") id ge p (dbf ns $ mkLets ge ds e) `SAppV` x    -- (p = e; f) -->  (\p -> f) e
+mkLets ge (ValueDef (ns, p) x: ds) e = patLam (debugSI "13") id ge p (dbff (map snd ns) $ mkLets ge ds e) `SAppV` x    -- (p = e; f) -->  (\p -> f) e
 mkLets _ (x: ds) e = error $ "mkLets: " ++ show x
 
 patLam si f ge = patLam_ si f ge (Visible, Wildcard SType)
@@ -2157,7 +2162,7 @@ parseSomeGuards ns f = do
     pos <- sourceColumn <$> getPosition <* reservedOp "|"
     guard $ f pos
     (e', f) <-
-         do (e', PCon (_, p) vs) <- try $ pattern' ns mempty <* reservedOp "<-"
+         do (e', PCon (_, p) vs) <- try $ pattern' ns <* reservedOp "<-"
             x <- parseETerm ns PrecEq
             return (e', \gs' gs -> GuardNode x p vs (Alts gs'): gs)
      <|> do x <- parseETerm ns PrecEq
@@ -2263,6 +2268,19 @@ varP = \case
     ViewPat e pp -> varPP pp
     PatType pp e -> varPP pp
 
+getPVars :: Pat -> DBNames
+getPVars = DBNamesC . reverse . getPVars_
+
+getPPVars = DBNamesC . reverse . getPPVars_
+
+getPVars_ = \case
+    PVar n -> [n]
+    PCon _ pp -> foldMap getPPVars_ pp
+    ViewPat e pp -> getPPVars_ pp
+    PatType pp e -> getPPVars_ pp
+
+getPPVars_ = \case
+    ParPat pp -> foldMap getPVars_ pp
 
 alts (Alts xs) = concatMap alts xs
 alts x = [x]
diff --git a/testdata/Builtins.out b/testdata/Builtins.out
index f84e8d03..dca1e33e 100644
--- a/testdata/Builtins.out
+++ b/testdata/Builtins.out
@@ -6,6 +6,9 @@ testdata/Builtins.lc 13:6-13:9  Type
 testdata/Builtins.lc 13:12-13:16  'Nat
 testdata/Builtins.lc 13:24-13:27  Type
 testdata/Builtins.lc 13:19-13:23  'Nat->'Nat
+testdata/Builtins.lc 13:6-13:23  Type
+testdata/Builtins.lc 13:19-13:23  Type
+testdata/Builtins.lc 13:19-13:23  'Nat
 testdata/Builtins.lc 15:6-15:10  Type->Type
 testdata/Builtins.lc 15:6-15:10  Type
 testdata/Builtins.lc 15:15-15:18  {a} -> 'List a
@@ -14,6 +17,10 @@ testdata/Builtins.lc 15:26-15:27  Type
 testdata/Builtins.lc 15:29-15:33  Type->Type
 testdata/Builtins.lc 15:34-15:35  Type
 testdata/Builtins.lc 15:21-15:25  {a} -> a -> 'List a -> 'List a
+testdata/Builtins.lc 15:6-15:25  Type
+testdata/Builtins.lc 15:15-15:18  'List V1
+testdata/Builtins.lc 15:21-15:25  Type
+testdata/Builtins.lc 15:21-15:25  'List V4
 testdata/Builtins.lc 19:26-23:31  Type -> Type->Type
 testdata/Builtins.lc 19:26-23:31  Type->Type
 testdata/Builtins.lc 19:26-23:31  Type
@@ -100,6 +107,14 @@ testdata/Builtins.lc 35:29-35:35  Type
 testdata/Builtins.lc 35:29-35:33  Type -> 'Nat->Type
 testdata/Builtins.lc 35:34-35:35  Type
 testdata/Builtins.lc 35:3-35:5  {a} -> a -> a -> a -> a -> 'VecS a (Succ (Succ (Succ (Succ Zero))))
+testdata/Builtins.lc 32:6-35:5  Type
+testdata/Builtins.lc 32:6-32:10  Type
+testdata/Builtins.lc 33:3-33:5  Type
+testdata/Builtins.lc 33:3-33:5  'VecS V3 (Succ (Succ Zero))
+testdata/Builtins.lc 34:3-34:5  Type
+testdata/Builtins.lc 34:3-34:5  'VecS V5 (Succ (Succ (Succ Zero)))
+testdata/Builtins.lc 35:3-35:5  Type
+testdata/Builtins.lc 35:3-35:5  'VecS V7 (Succ (Succ (Succ (Succ Zero))))
 testdata/Builtins.lc 37:23-37:26  Type
 testdata/Builtins.lc 37:47-37:55  'Nat -> Type->Type
 testdata/Builtins.lc 37:47-37:55  Type->Type
@@ -249,14 +264,26 @@ testdata/Builtins.lc 57:71-57:84  Type
 testdata/Builtins.lc 57:71-57:74  'Nat -> 'Nat -> Type->Type
 testdata/Builtins.lc 57:79-57:84  Type
 testdata/Builtins.lc 57:3-57:7  'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'Mat (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ (Succ Zero)))) 'Float
-testdata/Builtins.lc 49:49-57:84  Type
-testdata/Builtins.lc 50:49-57:84  Type
-testdata/Builtins.lc 51:49-57:84  Type
-testdata/Builtins.lc 52:64-57:84  Type
-testdata/Builtins.lc 53:64-57:84  Type
-testdata/Builtins.lc 54:64-57:84  Type
-testdata/Builtins.lc 55:79-57:84  Type
-testdata/Builtins.lc 56:79-57:84  Type
+testdata/Builtins.lc 48:6-48:9  Type
+testdata/Builtins.lc 48:6-57:84  Type
+testdata/Builtins.lc 49:3-49:54  Type
+testdata/Builtins.lc 49:3-49:7  'Mat (Succ (Succ Zero)) (Succ (Succ Zero)) 'Float
+testdata/Builtins.lc 50:3-50:54  Type
+testdata/Builtins.lc 50:3-50:7  'Mat (Succ (Succ (Succ Zero))) (Succ (Succ Zero)) 'Float
+testdata/Builtins.lc 51:3-51:54  Type
+testdata/Builtins.lc 51:3-51:7  'Mat (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ Zero)) 'Float
+testdata/Builtins.lc 52:3-52:69  Type
+testdata/Builtins.lc 52:3-52:7  'Mat (Succ (Succ Zero)) (Succ (Succ (Succ Zero))) 'Float
+testdata/Builtins.lc 53:3-53:69  Type
+testdata/Builtins.lc 53:3-53:7  'Mat (Succ (Succ (Succ Zero))) (Succ (Succ (Succ Zero))) 'Float
+testdata/Builtins.lc 54:3-54:69  Type
+testdata/Builtins.lc 54:3-54:7  'Mat (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ Zero))) 'Float
+testdata/Builtins.lc 55:3-55:84  Type
+testdata/Builtins.lc 55:3-55:7  'Mat (Succ (Succ Zero)) (Succ (Succ (Succ (Succ Zero)))) 'Float
+testdata/Builtins.lc 56:3-56:84  Type
+testdata/Builtins.lc 56:3-56:7  'Mat (Succ (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero)))) 'Float
+testdata/Builtins.lc 57:3-57:84  Type
+testdata/Builtins.lc 57:3-57:7  'Mat (Succ (Succ (Succ (Succ Zero)))) (Succ (Succ (Succ (Succ Zero)))) 'Float
 testdata/Builtins.lc 60:22-64:37  Type->Type
 testdata/Builtins.lc 60:22-64:37  Type
 testdata/Builtins.lc 60:30-60:35  Type
@@ -284,6 +311,7 @@ testdata/Builtins.lc 68:14-68:16  'Swizz
 testdata/Builtins.lc 68:19-68:21  'Swizz
 testdata/Builtins.lc 68:24-68:26  'Swizz
 testdata/Builtins.lc 68:29-68:31  'Swizz
+testdata/Builtins.lc 68:6-68:31  Type
 testdata/Builtins.lc 71:27-71:56  Type
 testdata/Builtins.lc 71:27-71:28  V5
 testdata/Builtins.lc 71:32-71:33  Type
@@ -898,12 +926,14 @@ testdata/Builtins.lc 202:7-202:28  'BlendingFactor
 testdata/Builtins.lc 203:7-203:20  'BlendingFactor
 testdata/Builtins.lc 204:7-204:28  'BlendingFactor
 testdata/Builtins.lc 205:7-205:23  'BlendingFactor
+testdata/Builtins.lc 190:6-205:23  Type
 testdata/Builtins.lc 207:6-207:19  Type
 testdata/Builtins.lc 208:7-208:14  'BlendEquation
 testdata/Builtins.lc 209:7-209:19  'BlendEquation
 testdata/Builtins.lc 210:7-210:26  'BlendEquation
 testdata/Builtins.lc 211:7-211:10  'BlendEquation
 testdata/Builtins.lc 212:7-212:10  'BlendEquation
+testdata/Builtins.lc 207:6-212:10  Type
 testdata/Builtins.lc 214:6-214:20  Type
 testdata/Builtins.lc 215:7-215:12  'LogicOperation
 testdata/Builtins.lc 216:7-216:10  'LogicOperation
@@ -921,6 +951,7 @@ testdata/Builtins.lc 227:7-227:19  'LogicOperation
 testdata/Builtins.lc 228:7-228:17  'LogicOperation
 testdata/Builtins.lc 229:7-229:11  'LogicOperation
 testdata/Builtins.lc 230:7-230:10  'LogicOperation
+testdata/Builtins.lc 214:6-230:10  Type
 testdata/Builtins.lc 232:6-232:22  Type
 testdata/Builtins.lc 233:7-233:13  'StencilOperation
 testdata/Builtins.lc 234:7-234:13  'StencilOperation
@@ -930,6 +961,7 @@ testdata/Builtins.lc 237:7-237:17  'StencilOperation
 testdata/Builtins.lc 238:7-238:13  'StencilOperation
 testdata/Builtins.lc 239:7-239:17  'StencilOperation
 testdata/Builtins.lc 240:7-240:15  'StencilOperation
+testdata/Builtins.lc 232:6-240:15  Type
 testdata/Builtins.lc 242:6-242:24  Type
 testdata/Builtins.lc 243:7-243:12  'ComparisonFunction
 testdata/Builtins.lc 244:7-244:11  'ComparisonFunction
@@ -939,41 +971,60 @@ testdata/Builtins.lc 247:7-247:14  'ComparisonFunction
 testdata/Builtins.lc 248:7-248:15  'ComparisonFunction
 testdata/Builtins.lc 249:7-249:13  'ComparisonFunction
 testdata/Builtins.lc 250:7-250:13  'ComparisonFunction
+testdata/Builtins.lc 242:6-250:13  Type
 testdata/Builtins.lc 252:6-252:21  Type
 testdata/Builtins.lc 253:7-253:17  'ProvokingVertex
 testdata/Builtins.lc 254:7-254:18  'ProvokingVertex
+testdata/Builtins.lc 252:6-254:18  Type
 testdata/Builtins.lc 256:6-256:14  Type
 testdata/Builtins.lc 257:7-257:16  'CullMode
 testdata/Builtins.lc 258:7-258:15  'CullMode
 testdata/Builtins.lc 259:7-259:15  'CullMode
+testdata/Builtins.lc 256:6-259:15  Type
 testdata/Builtins.lc 261:6-261:15  Type
 testdata/Builtins.lc 262:17-262:22  Type
 testdata/Builtins.lc 262:7-262:16  'Float->'PointSize
 testdata/Builtins.lc 263:7-263:23  'PointSize
+testdata/Builtins.lc 261:6-263:23  Type
+testdata/Builtins.lc 262:7-262:16  Type
+testdata/Builtins.lc 262:7-262:16  'PointSize
 testdata/Builtins.lc 265:6-265:17  Type
 testdata/Builtins.lc 266:7-266:18  'PolygonMode
 testdata/Builtins.lc 267:20-267:29  Type
 testdata/Builtins.lc 267:7-267:19  'PointSize->'PolygonMode
 testdata/Builtins.lc 268:19-268:24  Type
 testdata/Builtins.lc 268:7-268:18  'Float->'PolygonMode
+testdata/Builtins.lc 265:6-268:18  Type
+testdata/Builtins.lc 267:7-267:19  Type
+testdata/Builtins.lc 267:7-267:19  'PolygonMode
+testdata/Builtins.lc 268:7-268:18  Type
+testdata/Builtins.lc 268:7-268:18  'PolygonMode
 testdata/Builtins.lc 270:6-270:19  Type
 testdata/Builtins.lc 271:7-271:15  'PolygonOffset
 testdata/Builtins.lc 272:14-272:19  Type
 testdata/Builtins.lc 270:6-272:25  Type
 testdata/Builtins.lc 272:20-272:25  Type
 testdata/Builtins.lc 272:7-272:13  'Float -> 'Float->'PolygonOffset
+testdata/Builtins.lc 270:6-272:13  Type
+testdata/Builtins.lc 272:7-272:13  Type
+testdata/Builtins.lc 272:7-272:13  'PolygonOffset
 testdata/Builtins.lc 274:6-274:28  Type
 testdata/Builtins.lc 275:7-275:16  'PointSpriteCoordOrigin
 testdata/Builtins.lc 276:7-276:16  'PointSpriteCoordOrigin
+testdata/Builtins.lc 274:6-276:16  Type
 testdata/Builtins.lc 279:6-279:11  Type->Type
+testdata/Builtins.lc 279:6-279:11  Type
 testdata/Builtins.lc 280:6-280:13  Type->Type
+testdata/Builtins.lc 280:6-280:13  Type
 testdata/Builtins.lc 281:6-281:11  Type->Type
+testdata/Builtins.lc 281:6-281:11  Type
 testdata/Builtins.lc 283:6-283:19  Type
 testdata/Builtins.lc 284:7-284:15  'PrimitiveType
 testdata/Builtins.lc 285:7-285:11  'PrimitiveType
 testdata/Builtins.lc 286:7-286:12  'PrimitiveType
 testdata/Builtins.lc 287:7-287:24  'PrimitiveType
 testdata/Builtins.lc 288:7-288:20  'PrimitiveType
+testdata/Builtins.lc 283:6-288:20  Type
 testdata/Builtins.lc 291:16-291:18  Type
 testdata/Builtins.lc 291:22-291:48  Type
 testdata/Builtins.lc 291:22-291:25  'Nat -> Type->Type
@@ -1022,11 +1073,14 @@ testdata/Builtins.lc 300:89-300:107  Type
 testdata/Builtins.lc 300:89-300:102  'PrimitiveType->Type
 testdata/Builtins.lc 300:103-300:107  'PrimitiveType
 testdata/Builtins.lc 300:3-300:10  'Float -> 'ProvokingVertex -> 'RasterContext Line
-testdata/Builtins.lc 298:103-300:107  Type
-testdata/Builtins.lc 298:103-298:111  Type
-testdata/Builtins.lc 299:103-300:107  Type
-testdata/Builtins.lc 299:103-299:108  Type
-testdata/Builtins.lc 300:103-300:107  Type
+testdata/Builtins.lc 297:6-297:19  Type
+testdata/Builtins.lc 297:6-300:107  Type
+testdata/Builtins.lc 298:3-298:111  Type
+testdata/Builtins.lc 298:3-298:14  'RasterContext Triangle
+testdata/Builtins.lc 299:3-299:108  Type
+testdata/Builtins.lc 299:3-299:11  'RasterContext Point
+testdata/Builtins.lc 300:3-300:107  Type
+testdata/Builtins.lc 300:3-300:10  'RasterContext Line
 testdata/Builtins.lc 302:6-302:18  Type->Type
 testdata/Builtins.lc 304:27-304:56  Type
 testdata/Builtins.lc 304:27-304:35  Type->Type
@@ -1040,6 +1094,13 @@ testdata/Builtins.lc 305:42-305:56  Type
 testdata/Builtins.lc 305:42-305:54  Type->Type
 testdata/Builtins.lc 305:55-305:56  Type
 testdata/Builtins.lc 305:3-305:7  {a} -> 'Interpolated a
+testdata/Builtins.lc 302:6-305:7  Type
+testdata/Builtins.lc 303:3-303:9  Type
+testdata/Builtins.lc 303:3-303:9  'Interpolated V2
+testdata/Builtins.lc 303:11-303:24  Type
+testdata/Builtins.lc 303:11-303:24  'Interpolated V3
+testdata/Builtins.lc 305:3-305:7  'Interpolated V3
+testdata/Builtins.lc 302:6-302:18  Type
 testdata/Builtins.lc 309:14-310:32  Type->Type
 testdata/Builtins.lc 309:14-310:32  Type
 testdata/Builtins.lc 309:19-309:20  Type->Type
@@ -1115,8 +1176,14 @@ testdata/Builtins.lc 323:60-323:74  Type
 testdata/Builtins.lc 323:60-323:68  Type->Type
 testdata/Builtins.lc 323:69-323:74  Type
 testdata/Builtins.lc 321:3-321:8  'Tuple2 'BlendEquation 'BlendEquation -> 'Tuple2 ('Tuple2 'BlendingFactor 'BlendingFactor) ('Tuple2 'BlendingFactor 'BlendingFactor) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'Blending 'Float
-testdata/Builtins.lc 319:69-323:74  Type
-testdata/Builtins.lc 320:69-323:74  Type
+testdata/Builtins.lc 318:6-318:14  Type
+testdata/Builtins.lc 318:6-323:74  Type
+testdata/Builtins.lc 319:3-319:70  Type
+testdata/Builtins.lc 319:3-319:13  'Blending V0
+testdata/Builtins.lc 320:3-320:70  Type
+testdata/Builtins.lc 320:3-320:15  'Blending V2
+testdata/Builtins.lc 321:3-323:74  Type
+testdata/Builtins.lc 321:3-321:8  'Blending 'Float
 testdata/Builtins.lc 330:6-330:18  Type
 testdata/Builtins.lc 331:6-331:16  Type
 testdata/Builtins.lc 332:6-332:11  Type
@@ -1173,8 +1240,14 @@ testdata/Builtins.lc 338:90-338:103  Type
 testdata/Builtins.lc 338:90-338:97  Type->Type
 testdata/Builtins.lc 338:98-338:103  Type
 testdata/Builtins.lc 338:3-338:12  'StencilTests -> 'StencilOps -> 'StencilOps -> 'FragmentOperation ('Stencil 'Int32)
-testdata/Builtins.lc 336:90-338:103  Type
-testdata/Builtins.lc 337:90-338:103  Type
+testdata/Builtins.lc 334:6-334:23  Type
+testdata/Builtins.lc 334:6-338:103  Type
+testdata/Builtins.lc 335:3-336:101  Type
+testdata/Builtins.lc 335:3-335:10  'FragmentOperation ('Color V6)
+testdata/Builtins.lc 337:3-337:101  Type
+testdata/Builtins.lc 337:3-337:10  'FragmentOperation ('Depth 'Float)
+testdata/Builtins.lc 338:3-338:103  Type
+testdata/Builtins.lc 338:3-338:12  'FragmentOperation ('Stencil 'Int32)
 testdata/Builtins.lc 341:32-345:146  Type->Type
 testdata/Builtins.lc 341:32-345:146  Type
 testdata/Builtins.lc 341:37-341:38  Type->Type
@@ -1295,6 +1368,7 @@ testdata/Builtins.lc 352:19-352:36  Type->Type
 testdata/Builtins.lc 352:37-352:38  Type
 testdata/Builtins.lc 348:5-348:13  Type->Type
 testdata/Builtins.lc 354:6-354:12  Type->Type
+testdata/Builtins.lc 354:6-354:12  Type
 testdata/Builtins.lc 356:15-356:46  Type
 testdata/Builtins.lc 356:15-356:16  V3
 testdata/Builtins.lc 356:20-356:21  Type
@@ -1331,6 +1405,7 @@ testdata/Builtins.lc 358:51-358:52  Type
 testdata/Builtins.lc 358:1-358:13  {a} -> a->'Bool -> 'Stream a -> 'Stream a
 testdata/Builtins.lc 360:22-360:35  Type
 testdata/Builtins.lc 360:6-360:15  'PrimitiveType -> Type->Type
+testdata/Builtins.lc 360:6-360:15  Type
 testdata/Builtins.lc 362:28-362:34  Type->Type
 testdata/Builtins.lc 362:36-362:49  Type
 testdata/Builtins.lc 362:36-362:45  'PrimitiveType -> Type->Type
@@ -1512,6 +1587,7 @@ testdata/Builtins.lc 389:25-389:37  Type
 testdata/Builtins.lc 389:25-389:29  Type
 testdata/Builtins.lc 389:33-389:37  Type
 testdata/Builtins.lc 389:6-389:14  'Nat -> Type->Type
+testdata/Builtins.lc 389:6-389:14  Type
 testdata/Builtins.lc 391:27-391:33  Type->Type
 testdata/Builtins.lc 391:35-391:47  Type
 testdata/Builtins.lc 391:35-391:43  'Nat -> Type->Type
@@ -1719,6 +1795,12 @@ testdata/Builtins.lc 433:102-433:113  'Nat -> Type->Type
 testdata/Builtins.lc 433:114-433:115  'Nat
 testdata/Builtins.lc 433:116-433:117  Type
 testdata/Builtins.lc 433:3-433:14  {a:'Nat} -> {b} -> {c} -> {d : 'SameLayerCounts c} -> {e : 'FrameBuffer a b ~ 'TFFrameBuffer c} -> c -> 'FrameBuffer a b
+testdata/Builtins.lc 431:6-433:14  Type
+testdata/Builtins.lc 432:3-432:13  Type
+testdata/Builtins.lc 432:3-432:13  'FrameBuffer V5 V4
+testdata/Builtins.lc 433:3-433:14  Type
+testdata/Builtins.lc 433:3-433:14  'FrameBuffer V7 V6
+testdata/Builtins.lc 431:6-431:17  Type
 testdata/Builtins.lc 435:34-435:44  {a:'Nat} -> {b} -> 'FragOps' b -> 'Stream ('Fragment a ('RemSemantics b)) -> 'FrameBuffer a b -> 'FrameBuffer a b
 testdata/Builtins.lc 435:45-435:48  'FragOps' V0
 testdata/Builtins.lc 435:45-435:48  V9
@@ -1807,13 +1889,18 @@ testdata/Builtins.lc 447:94-447:105  Type
 testdata/Builtins.lc 447:94-447:97  'Nat -> Type->Type
 testdata/Builtins.lc 447:100-447:105  Type
 testdata/Builtins.lc 447:3-447:16  'FrameBuffer (Succ Zero) ('Tuple2 ('Depth 'Float) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))))) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))))
-testdata/Builtins.lc 441:42-447:105  Type
-testdata/Builtins.lc 441:42-441:56  Type
-testdata/Builtins.lc 442:53-447:105  Type
-testdata/Builtins.lc 442:53-442:67  Type
-testdata/Builtins.lc 443:53-447:105  Type
-testdata/Builtins.lc 443:53-443:67  Type
-testdata/Builtins.lc 446:53-447:105  Type
+testdata/Builtins.lc 439:6-439:11  Type
+testdata/Builtins.lc 439:6-447:105  Type
+testdata/Builtins.lc 440:3-441:56  Type
+testdata/Builtins.lc 440:3-440:13  'Image V6 ('Color V3)
+testdata/Builtins.lc 442:3-442:67  Type
+testdata/Builtins.lc 442:3-442:13  'Image V1 ('Depth 'Float)
+testdata/Builtins.lc 443:3-443:67  Type
+testdata/Builtins.lc 443:3-443:15  'Image V1 ('Stencil 'Int)
+testdata/Builtins.lc 446:3-446:54  Type
+testdata/Builtins.lc 446:3-446:11  'Image (Succ Zero) V1
+testdata/Builtins.lc 447:3-447:105  Type
+testdata/Builtins.lc 447:3-447:16  'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero))))))
 testdata/Builtins.lc 449:6-449:12  Type
 testdata/Builtins.lc 450:26-450:51  Type
 testdata/Builtins.lc 450:26-450:37  'Nat -> Type->Type
@@ -1823,6 +1910,9 @@ testdata/Builtins.lc 450:40-450:41  Type
 testdata/Builtins.lc 450:40-450:41  V1
 testdata/Builtins.lc 450:45-450:51  Type
 testdata/Builtins.lc 450:3-450:12  {a:'Nat} -> {b} -> 'FrameBuffer a b -> 'Output
+testdata/Builtins.lc 449:6-450:12  Type
+testdata/Builtins.lc 450:3-450:12  Type
+testdata/Builtins.lc 450:3-450:12  'Output
 testdata/Builtins.lc 456:34-456:73  Type
 testdata/Builtins.lc 456:34-456:37  Type->Type
 testdata/Builtins.lc 456:39-456:57  Type
@@ -2675,19 +2765,29 @@ testdata/Builtins.lc 546:36-546:39  'Nat -> Type->Type
 testdata/Builtins.lc 546:42-546:47  Type
 testdata/Builtins.lc 547:20-547:27  Type
 testdata/Builtins.lc 545:3-545:12  'VecS 'Int (Succ (Succ Zero)) -> 'Image (Succ Zero) ('Color ('VecS 'Float (Succ (Succ (Succ (Succ Zero)))))) -> 'Texture
+testdata/Builtins.lc 541:6-545:12  Type
+testdata/Builtins.lc 542:3-542:16  Type
+testdata/Builtins.lc 542:3-542:16  'Texture
+testdata/Builtins.lc 545:3-545:12  Type
+testdata/Builtins.lc 545:3-545:12  'Texture
 testdata/Builtins.lc 549:6-549:12  Type
 testdata/Builtins.lc 550:5-550:16  'Filter
 testdata/Builtins.lc 551:5-551:17  'Filter
+testdata/Builtins.lc 549:6-551:17  Type
 testdata/Builtins.lc 553:6-553:14  Type
 testdata/Builtins.lc 554:5-554:11  'EdgeMode
 testdata/Builtins.lc 555:5-555:19  'EdgeMode
 testdata/Builtins.lc 556:5-556:16  'EdgeMode
+testdata/Builtins.lc 553:6-556:16  Type
 testdata/Builtins.lc 558:6-558:13  Type
 testdata/Builtins.lc 558:24-558:30  Type
 testdata/Builtins.lc 558:6-558:47  Type
 testdata/Builtins.lc 558:31-558:39  Type
 testdata/Builtins.lc 558:40-558:47  Type
 testdata/Builtins.lc 558:16-558:23  'Filter -> 'EdgeMode -> 'Texture->'Sampler
+testdata/Builtins.lc 558:6-558:23  Type
+testdata/Builtins.lc 558:16-558:23  Type
+testdata/Builtins.lc 558:16-558:23  'Sampler
 testdata/Builtins.lc 561:14-561:21  Type
 testdata/Builtins.lc 561:25-561:51  Type
 testdata/Builtins.lc 561:25-561:28  'Nat -> Type->Type
diff --git a/testdata/Internals.out b/testdata/Internals.out
index 06279002..d879bffd 100644
--- a/testdata/Internals.out
+++ b/testdata/Internals.out
@@ -11,22 +11,31 @@ testdata/Internals.lc 7:45-7:46  Type
 testdata/Internals.lc 7:1-7:8  {a} -> a->a -> a
 testdata/Internals.lc 9:6-9:10  Type
 testdata/Internals.lc 9:13-9:15  'Unit
+testdata/Internals.lc 9:6-9:15  Type
 testdata/Internals.lc 10:6-10:12  Type
 testdata/Internals.lc 11:18-11:24  Type
 testdata/Internals.lc 11:6-11:11  'String->Type
+testdata/Internals.lc 11:6-11:11  Type
 testdata/Internals.lc 14:6-14:12  Type
 testdata/Internals.lc 14:15-14:21  'Tuple0
+testdata/Internals.lc 14:6-14:21  Type
 testdata/Internals.lc 15:6-15:12  Type->Type
 testdata/Internals.lc 15:6-15:25  Type
 testdata/Internals.lc 15:24-15:25  Type
 testdata/Internals.lc 15:6-15:12  Type
 testdata/Internals.lc 15:17-15:23  {a} -> a -> 'Tuple1 a
+testdata/Internals.lc 15:6-15:23  Type
+testdata/Internals.lc 15:17-15:23  Type
+testdata/Internals.lc 15:17-15:23  'Tuple1 V2
 testdata/Internals.lc 16:6-16:12  Type -> Type->Type
 testdata/Internals.lc 16:6-16:29  Type
 testdata/Internals.lc 16:26-16:27  Type
 testdata/Internals.lc 16:28-16:29  Type
 testdata/Internals.lc 16:6-16:12  Type
 testdata/Internals.lc 16:19-16:25  {a} -> {b} -> a -> b -> 'Tuple2 a b
+testdata/Internals.lc 16:6-16:25  Type
+testdata/Internals.lc 16:19-16:25  Type
+testdata/Internals.lc 16:19-16:25  'Tuple2 V4 V3
 testdata/Internals.lc 17:6-17:12  Type -> Type -> Type->Type
 testdata/Internals.lc 17:6-17:33  Type
 testdata/Internals.lc 17:28-17:29  Type
@@ -34,6 +43,9 @@ testdata/Internals.lc 17:30-17:31  Type
 testdata/Internals.lc 17:32-17:33  Type
 testdata/Internals.lc 17:6-17:12  Type
 testdata/Internals.lc 17:21-17:27  {a} -> {b} -> {c} -> a -> b -> c -> 'Tuple3 a b c
+testdata/Internals.lc 17:6-17:27  Type
+testdata/Internals.lc 17:21-17:27  Type
+testdata/Internals.lc 17:21-17:27  'Tuple3 V6 V5 V4
 testdata/Internals.lc 18:6-18:12  Type -> Type -> Type -> Type->Type
 testdata/Internals.lc 18:6-18:37  Type
 testdata/Internals.lc 18:30-18:31  Type
@@ -42,6 +54,9 @@ testdata/Internals.lc 18:34-18:35  Type
 testdata/Internals.lc 18:36-18:37  Type
 testdata/Internals.lc 18:6-18:12  Type
 testdata/Internals.lc 18:23-18:29  {a} -> {b} -> {c} -> {d} -> a -> b -> c -> d -> 'Tuple4 a b c d
+testdata/Internals.lc 18:6-18:29  Type
+testdata/Internals.lc 18:23-18:29  Type
+testdata/Internals.lc 18:23-18:29  'Tuple4 V8 V7 V6 V5
 testdata/Internals.lc 19:6-19:12  Type -> Type -> Type -> Type -> Type->Type
 testdata/Internals.lc 19:6-19:41  Type
 testdata/Internals.lc 19:32-19:33  Type
@@ -51,6 +66,9 @@ testdata/Internals.lc 19:38-19:39  Type
 testdata/Internals.lc 19:40-19:41  Type
 testdata/Internals.lc 19:6-19:12  Type
 testdata/Internals.lc 19:25-19:31  {a} -> {b} -> {c} -> {d} -> {e} -> a -> b -> c -> d -> e -> 'Tuple5 a b c d e
+testdata/Internals.lc 19:6-19:31  Type
+testdata/Internals.lc 19:25-19:31  Type
+testdata/Internals.lc 19:25-19:31  'Tuple5 V10 V9 V8 V7 V6
 testdata/Internals.lc 25:24-25:35  Type
 testdata/Internals.lc 25:24-25:25  V1
 testdata/Internals.lc 25:29-25:35  Type
@@ -75,10 +93,12 @@ testdata/Internals.lc 37:6-37:10  Type
 testdata/Internals.lc 39:6-39:10  Type
 testdata/Internals.lc 39:13-39:18  'Bool
 testdata/Internals.lc 39:21-39:25  'Bool
+testdata/Internals.lc 39:6-39:25  Type
 testdata/Internals.lc 41:6-41:14  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 41:6-41:29  Type
 testdata/Internals.lc 44:24-44:27  Type
 testdata/Internals.lc 44:33-44:37  Type
 testdata/Internals.lc 44:1-44:14  'Int->'Word
diff --git a/testdata/Material.out b/testdata/Material.out
index b752ab32..4919e496 100644
--- a/testdata/Material.out
+++ b/testdata/Material.out
@@ -15,16 +15,19 @@ testdata/Material.lc 14:34-14:39  Type
 testdata/Material.lc 15:28-15:31  'Nat -> Type->Type
 testdata/Material.lc 15:34-15:39  Type
 testdata/Material.lc 11:7-11:13  'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'Entity
+testdata/Material.lc 10:6-11:13  Type
+testdata/Material.lc 11:7-11:13  Type
+testdata/Material.lc 11:7-11:13  'Entity
 testdata/Material.lc 11:7-11:13  'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> V4
 testdata/Material.lc 11:7-11:13  'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> V4
 testdata/Material.lc 11:7-11:13  'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> V4
 testdata/Material.lc 11:7-11:13  'VecS 'Float (Succ (Succ (Succ (Succ Zero)))) -> V4
 testdata/Material.lc 11:7-11:13  V4
-testdata/Material.lc 11:7-11:13  'VecS 'Float (Succ (Succ (Succ Zero)))
-testdata/Material.lc 11:7-11:13  'Entity
+testdata/Material.lc 11:7-11:13  'VecS 'Float (Succ (Succ (Succ (Succ Zero))))
 testdata/Material.lc 11:7-11:13  V1
+testdata/Material.lc 15:7-15:18  'Entity -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero))))
+testdata/Material.lc 11:7-11:13  'VecS 'Float (Succ (Succ (Succ Zero)))
 testdata/Material.lc 14:7-14:16  'Entity -> 'VecS 'Float (Succ (Succ (Succ Zero)))
-testdata/Material.lc 11:7-11:13  'VecS 'Float (Succ (Succ (Succ (Succ Zero))))
 testdata/Material.lc 13:7-13:21  'Entity -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero))))
 testdata/Material.lc 12:7-12:20  'Entity -> 'VecS 'Float (Succ (Succ (Succ (Succ Zero))))
 testdata/Material.lc 18:6-18:14  Type
@@ -34,6 +37,7 @@ testdata/Material.lc 21:7-21:16  'WaveType
 testdata/Material.lc 22:7-22:18  'WaveType
 testdata/Material.lc 23:7-23:25  'WaveType
 testdata/Material.lc 24:7-24:15  'WaveType
+testdata/Material.lc 18:6-24:15  Type
 testdata/Material.lc 27:6-27:10  Type
 testdata/Material.lc 27:18-27:26  Type
 testdata/Material.lc 27:6-27:50  Type
@@ -42,6 +46,9 @@ testdata/Material.lc 27:33-27:38  Type
 testdata/Material.lc 27:39-27:44  Type
 testdata/Material.lc 27:45-27:50  Type
 testdata/Material.lc 27:13-27:17  'WaveType -> 'Float -> 'Float -> 'Float -> 'Float->'Wave
+testdata/Material.lc 27:6-27:17  Type
+testdata/Material.lc 27:13-27:17  Type
+testdata/Material.lc 27:13-27:17  'Wave
 testdata/Material.lc 29:6-29:12  Type
 testdata/Material.lc 30:7-30:19  'Deform
 testdata/Material.lc 31:7-31:20  'Deform
@@ -72,10 +79,20 @@ testdata/Material.lc 44:14-44:19  Type
 testdata/Material.lc 29:6-44:24  Type
 testdata/Material.lc 44:20-44:24  Type
 testdata/Material.lc 44:7-44:13  'Float -> 'Wave->'Deform
+testdata/Material.lc 29:6-44:13  Type
+testdata/Material.lc 32:7-32:14  Type
+testdata/Material.lc 32:7-32:14  'Deform
+testdata/Material.lc 33:7-33:13  Type
+testdata/Material.lc 33:7-33:13  'Deform
+testdata/Material.lc 34:7-34:15  Type
+testdata/Material.lc 34:7-34:15  'Deform
+testdata/Material.lc 44:7-44:13  Type
+testdata/Material.lc 44:7-44:13  'Deform
 testdata/Material.lc 47:6-47:14  Type
 testdata/Material.lc 48:7-48:20  'CullType
 testdata/Material.lc 49:7-49:19  'CullType
 testdata/Material.lc 50:7-50:18  'CullType
+testdata/Material.lc 47:6-50:18  Type
 testdata/Material.lc 53:6-53:15  Type
 testdata/Material.lc 54:7-54:17  'Blending'
 testdata/Material.lc 55:7-55:17  'Blending'
@@ -88,6 +105,7 @@ testdata/Material.lc 61:7-61:17  'Blending'
 testdata/Material.lc 62:7-62:25  'Blending'
 testdata/Material.lc 63:7-63:17  'Blending'
 testdata/Material.lc 64:7-64:13  'Blending'
+testdata/Material.lc 53:6-64:13  Type
 testdata/Material.lc 67:6-67:12  Type
 testdata/Material.lc 68:16-68:20  Type
 testdata/Material.lc 68:7-68:15  'Wave->'RGBGen
@@ -105,6 +123,11 @@ testdata/Material.lc 75:7-75:17  'RGBGen
 testdata/Material.lc 76:7-76:26  'RGBGen
 testdata/Material.lc 77:7-77:25  'RGBGen
 testdata/Material.lc 78:7-78:20  'RGBGen
+testdata/Material.lc 67:6-78:20  Type
+testdata/Material.lc 68:7-68:15  Type
+testdata/Material.lc 68:7-68:15  'RGBGen
+testdata/Material.lc 69:7-69:16  Type
+testdata/Material.lc 69:7-69:16  'RGBGen
 testdata/Material.lc 81:6-81:14  Type
 testdata/Material.lc 82:14-82:18  Type
 testdata/Material.lc 82:7-82:13  'Wave->'AlphaGen
@@ -117,6 +140,11 @@ testdata/Material.lc 87:7-87:23  'AlphaGen
 testdata/Material.lc 88:7-88:15  'AlphaGen
 testdata/Material.lc 89:7-89:25  'AlphaGen
 testdata/Material.lc 90:7-90:23  'AlphaGen
+testdata/Material.lc 81:6-90:23  Type
+testdata/Material.lc 82:7-82:13  Type
+testdata/Material.lc 82:7-82:13  'AlphaGen
+testdata/Material.lc 83:7-83:14  Type
+testdata/Material.lc 83:7-83:14  'AlphaGen
 testdata/Material.lc 93:6-93:11  Type
 testdata/Material.lc 94:7-94:14  'TCGen
 testdata/Material.lc 95:7-95:18  'TCGen
@@ -128,6 +156,9 @@ testdata/Material.lc 97:32-97:35  'Nat -> Type->Type
 testdata/Material.lc 97:38-97:43  Type
 testdata/Material.lc 97:7-97:16  'VecS 'Float (Succ (Succ (Succ Zero))) -> 'VecS 'Float (Succ (Succ (Succ Zero))) -> 'TCGen
 testdata/Material.lc 98:7-98:19  'TCGen
+testdata/Material.lc 93:6-98:19  Type
+testdata/Material.lc 97:7-97:16  Type
+testdata/Material.lc 97:7-97:16  'TCGen
 testdata/Material.lc 101:6-101:11  Type
 testdata/Material.lc 102:7-102:25  'TCMod
 testdata/Material.lc 103:17-103:22  Type
@@ -156,6 +187,19 @@ testdata/Material.lc 108:21-108:26  Type
 testdata/Material.lc 108:27-108:32  Type
 testdata/Material.lc 108:33-108:38  Type
 testdata/Material.lc 108:7-108:14  'Float -> 'Float -> 'Float -> 'Float->'TCMod
+testdata/Material.lc 101:6-108:14  Type
+testdata/Material.lc 103:7-103:16  Type
+testdata/Material.lc 103:7-103:16  'TCMod
+testdata/Material.lc 104:7-104:16  Type
+testdata/Material.lc 104:7-104:16  'TCMod
+testdata/Material.lc 105:7-105:15  Type
+testdata/Material.lc 105:7-105:15  'TCMod
+testdata/Material.lc 106:7-106:17  Type
+testdata/Material.lc 106:7-106:17  'TCMod
+testdata/Material.lc 107:7-107:19  Type
+testdata/Material.lc 107:7-107:19  'TCMod
+testdata/Material.lc 108:7-108:14  Type
+testdata/Material.lc 108:7-108:14  'TCMod
 testdata/Material.lc 111:6-111:18  Type
 testdata/Material.lc 112:21-112:27  Type
 testdata/Material.lc 112:7-112:13  'String->'StageTexture
@@ -167,13 +211,22 @@ testdata/Material.lc 114:28-114:34  Type
 testdata/Material.lc 114:7-114:17  'Float -> 'List 'String -> 'StageTexture
 testdata/Material.lc 115:7-115:18  'StageTexture
 testdata/Material.lc 116:7-116:20  'StageTexture
+testdata/Material.lc 111:6-116:20  Type
+testdata/Material.lc 112:7-112:13  Type
+testdata/Material.lc 112:7-112:13  'StageTexture
+testdata/Material.lc 113:7-113:18  Type
+testdata/Material.lc 113:7-113:18  'StageTexture
+testdata/Material.lc 114:7-114:17  Type
+testdata/Material.lc 114:7-114:17  'StageTexture
 testdata/Material.lc 119:6-119:19  Type
 testdata/Material.lc 120:7-120:12  'AlphaFunction
 testdata/Material.lc 121:7-121:14  'AlphaFunction
 testdata/Material.lc 122:7-122:14  'AlphaFunction
+testdata/Material.lc 119:6-122:14  Type
 testdata/Material.lc 125:6-125:19  Type
 testdata/Material.lc 126:7-126:14  'DepthFunction
 testdata/Material.lc 127:7-127:15  'DepthFunction
+testdata/Material.lc 125:6-127:15  Type
 testdata/Material.lc 130:6-130:16  Type
 testdata/Material.lc 132:25-132:30  Type->Type
 testdata/Material.lc 132:31-132:53  Type
@@ -193,6 +246,9 @@ testdata/Material.lc 140:31-140:44  Type
 testdata/Material.lc 143:32-143:36  Type
 testdata/Material.lc 144:28-144:34  Type
 testdata/Material.lc 131:7-131:17  'Maybe ('Tuple2 'Blending' 'Blending') -> 'RGBGen -> 'AlphaGen -> 'TCGen -> 'List 'TCMod -> 'StageTexture -> 'Bool -> 'DepthFunction -> 'Maybe 'AlphaFunction -> 'Bool -> 'String->'StageAttrs
+testdata/Material.lc 130:6-131:17  Type
+testdata/Material.lc 131:7-131:17  Type
+testdata/Material.lc 131:7-131:17  'StageAttrs
 testdata/Material.lc 131:7-131:17  'Maybe ('Tuple2 'Blending' 'Blending') -> 'RGBGen -> 'AlphaGen -> 'TCGen -> 'List 'TCMod -> 'StageTexture -> 'Bool -> 'DepthFunction -> 'Maybe 'AlphaFunction -> 'Bool -> 'String->V11
 testdata/Material.lc 131:7-131:17  'RGBGen -> 'AlphaGen -> 'TCGen -> 'List 'TCMod -> 'StageTexture -> 'Bool -> 'DepthFunction -> 'Maybe 'AlphaFunction -> 'Bool -> 'String->V11
 testdata/Material.lc 131:7-131:17  'AlphaGen -> 'TCGen -> 'List 'TCMod -> 'StageTexture -> 'Bool -> 'DepthFunction -> 'Maybe 'AlphaFunction -> 'Bool -> 'String->V11
@@ -205,9 +261,10 @@ testdata/Material.lc 131:7-131:17  'Maybe 'AlphaFunction -> 'Bool -> 'String->V1
 testdata/Material.lc 131:7-131:17  'Bool -> 'String->V11
 testdata/Material.lc 131:7-131:17  'String->V11
 testdata/Material.lc 131:7-131:17  V11
-testdata/Material.lc 131:7-131:17  'Bool
-testdata/Material.lc 131:7-131:17  'StageAttrs
+testdata/Material.lc 131:7-131:17  'String
 testdata/Material.lc 131:7-131:17  V1
+testdata/Material.lc 144:7-144:23  'StageAttrs->'String
+testdata/Material.lc 131:7-131:17  'Bool
 testdata/Material.lc 143:7-143:26  'StageAttrs->'Bool
 testdata/Material.lc 131:7-131:17  'Maybe 'AlphaFunction
 testdata/Material.lc 140:7-140:18  'StageAttrs -> 'Maybe 'AlphaFunction
@@ -257,6 +314,9 @@ testdata/Material.lc 174:28-174:32  Type
 testdata/Material.lc 175:29-175:39  Type
 testdata/Material.lc 178:28-178:32  Type
 testdata/Material.lc 164:7-164:18  'Tuple0 -> 'Tuple0 -> 'Bool -> 'Int -> 'Bool -> 'Bool -> 'CullType -> 'List 'Deform -> 'Bool -> 'Bool -> 'List 'StageAttrs -> 'Bool->'CommonAttrs
+testdata/Material.lc 163:6-164:18  Type
+testdata/Material.lc 164:7-164:18  Type
+testdata/Material.lc 164:7-164:18  'CommonAttrs
 testdata/Material.lc 164:7-164:18  'Tuple0 -> 'Tuple0 -> 'Bool -> 'Int -> 'Bool -> 'Bool -> 'CullType -> 'List 'Deform -> 'Bool -> 'Bool -> 'List 'StageAttrs -> 'Bool->V12
 testdata/Material.lc 164:7-164:18  'Tuple0 -> 'Bool -> 'Int -> 'Bool -> 'Bool -> 'CullType -> 'List 'Deform -> 'Bool -> 'Bool -> 'List 'StageAttrs -> 'Bool->V12
 testdata/Material.lc 164:7-164:18  'Bool -> 'Int -> 'Bool -> 'Bool -> 'CullType -> 'List 'Deform -> 'Bool -> 'Bool -> 'List 'StageAttrs -> 'Bool->V12
@@ -270,11 +330,11 @@ testdata/Material.lc 164:7-164:18  'Bool -> 'List 'StageAttrs -> 'Bool->V12
 testdata/Material.lc 164:7-164:18  'List 'StageAttrs -> 'Bool->V12
 testdata/Material.lc 164:7-164:18  'Bool->V12
 testdata/Material.lc 164:7-164:18  V12
-testdata/Material.lc 164:7-164:18  'List 'StageAttrs
-testdata/Material.lc 164:7-164:18  'CommonAttrs
+testdata/Material.lc 164:7-164:18  'Bool
 testdata/Material.lc 164:7-164:18  V1
+testdata/Material.lc 178:7-178:14  'CommonAttrs->'Bool
+testdata/Material.lc 164:7-164:18  'List 'StageAttrs
 testdata/Material.lc 175:7-175:15  'CommonAttrs -> 'List 'StageAttrs
-testdata/Material.lc 164:7-164:18  'Bool
 testdata/Material.lc 174:7-174:22  'CommonAttrs->'Bool
 testdata/Material.lc 173:7-173:18  'CommonAttrs->'Bool
 testdata/Material.lc 164:7-164:18  'List 'Deform
diff --git a/testdata/Prelude.out b/testdata/Prelude.out
index 4af75bcd..17c94c1c 100644
--- a/testdata/Prelude.out
+++ b/testdata/Prelude.out
@@ -406,6 +406,10 @@ testdata/Prelude.lc 91:7-91:14  {a} -> 'Maybe a
 testdata/Prelude.lc 90:6-92:13  Type
 testdata/Prelude.lc 92:12-92:13  Type
 testdata/Prelude.lc 92:7-92:11  {a} -> a -> 'Maybe a
+testdata/Prelude.lc 90:6-92:11  Type
+testdata/Prelude.lc 91:7-91:14  'Maybe V1
+testdata/Prelude.lc 92:7-92:11  Type
+testdata/Prelude.lc 92:7-92:11  'Maybe V3
 testdata/Prelude.lc 96:14-96:15  V2 -> V2->V2
 testdata/Prelude.lc 96:14-96:15  V2->V2
 testdata/Prelude.lc 96:14-96:15  V2
@@ -455,6 +459,9 @@ testdata/Prelude.lc 104:36-104:38  'List ('Tuple2 V0 Type)
 testdata/Prelude.lc 104:36-104:38  'List ('Tuple2 'String Type)
 testdata/Prelude.lc 103:6-103:13  Type
 testdata/Prelude.lc 104:7-104:17  {a : 'List ('Tuple2 'String Type)} -> tuptype (map ('Tuple2 'String Type) Type (\(b : 'Tuple2 'String Type) -> snd 'String Type b) a) -> 'RecordC a
+testdata/Prelude.lc 103:6-104:17  Type
+testdata/Prelude.lc 104:7-104:17  Type
+testdata/Prelude.lc 104:7-104:17  'RecordC V2
 testdata/Prelude.lc 106:1-106:7  {a} -> a->a -> a
 testdata/Prelude.lc 106:11-107:36  V0->V1
 testdata/Prelude.lc 106:11-107:36  V1
diff --git a/testdata/ambig.out b/testdata/ambig.out
index 6c9fb611..e309814c 100644
--- a/testdata/ambig.out
+++ b/testdata/ambig.out
@@ -6,6 +6,9 @@ testdata/ambig.lc 3:26-3:27  Type
 testdata/ambig.lc 3:28-3:29  Type
 testdata/ambig.lc 3:6-3:12  Type
 testdata/ambig.lc 3:19-3:25  {a} -> {b} -> a -> b -> 'Tuple2 a b
+testdata/ambig.lc 3:6-3:25  Type
+testdata/ambig.lc 3:19-3:25  Type
+testdata/ambig.lc 3:19-3:25  'Tuple2 V4 V3
 testdata/ambig.lc 8:21-8:26  V2 -> V2->V2
 testdata/ambig.lc 8:21-8:26  V2->V2
 testdata/ambig.lc 8:21-8:26  V2
diff --git a/testdata/complex.out b/testdata/complex.out
index 9a824fdc..083010e5 100644
--- a/testdata/complex.out
+++ b/testdata/complex.out
@@ -3,6 +3,7 @@ tooltips:
 testdata/complex.lc 3:6-3:10  Type
 testdata/complex.lc 3:13-3:19  'Repr
 testdata/complex.lc 3:22-3:27  'Repr
+testdata/complex.lc 3:6-3:27  Type
 testdata/complex.lc 5:17-5:21  Type
 testdata/complex.lc 5:25-5:29  Type
 testdata/complex.lc 5:6-5:13  'Repr->Type
@@ -15,7 +16,10 @@ testdata/complex.lc 6:43-6:50  'Repr->Type
 testdata/complex.lc 6:51-6:52  'Repr
 testdata/complex.lc 6:51-6:52  V3
 testdata/complex.lc 6:3-6:10  {a:'Repr} -> 'Float -> 'Float -> 'Complex a
-testdata/complex.lc 6:51-6:52  Type
+testdata/complex.lc 5:6-5:13  Type
+testdata/complex.lc 5:6-6:52  Type
+testdata/complex.lc 6:3-6:52  Type
+testdata/complex.lc 6:3-6:10  'Complex V2
 testdata/complex.lc 8:20-8:37  Type
 testdata/complex.lc 8:20-8:27  'Repr->Type
 testdata/complex.lc 8:28-8:29  'Repr
diff --git a/testdata/data.out b/testdata/data.out
index ab8765f8..97814586 100644
--- a/testdata/data.out
+++ b/testdata/data.out
@@ -2,6 +2,7 @@ main is not found
 tooltips:
 testdata/data.lc 1:6-1:11  Type
 testdata/data.lc 1:14-1:19  'Data0
+testdata/data.lc 1:6-1:19  Type
 testdata/data.lc 3:6-3:11  Type -> Type -> Type->Type
 testdata/data.lc 3:6-3:31  Type
 testdata/data.lc 3:26-3:27  Type
@@ -9,6 +10,9 @@ testdata/data.lc 3:28-3:29  Type
 testdata/data.lc 3:30-3:31  Type
 testdata/data.lc 3:6-3:11  Type
 testdata/data.lc 3:20-3:25  {a} -> {b} -> {c} -> a -> b -> c -> 'Data1 a b c
+testdata/data.lc 3:6-3:25  Type
+testdata/data.lc 3:20-3:25  Type
+testdata/data.lc 3:20-3:25  'Data1 V6 V5 V4
 testdata/data.lc 5:6-5:11  Type
 testdata/data.lc 5:21-5:24  Type
 testdata/data.lc 5:14-5:20  'Int->'Data2
@@ -19,13 +23,24 @@ testdata/data.lc 6:14-6:20  'Int -> 'Int->'Data2
 testdata/data.lc 7:28-7:31  Type
 testdata/data.lc 7:14-7:20  'Int->'Data2
 testdata/data.lc 8:14-8:20  'Data2
+testdata/data.lc 5:6-8:20  Type
+testdata/data.lc 5:14-5:20  Type
+testdata/data.lc 5:14-5:20  'Data2
+testdata/data.lc 6:14-6:20  Type
+testdata/data.lc 6:14-6:20  'Data2
+testdata/data.lc 7:14-7:20  Type
+testdata/data.lc 7:14-7:20  'Data2
 testdata/data.lc 6:14-6:20  'Int -> 'Int->V2
 testdata/data.lc 6:14-6:20  'Int->V2
 testdata/data.lc 6:14-6:20  V2
 testdata/data.lc 6:14-6:20  'Int
-testdata/data.lc 6:14-6:20  'Data2
 testdata/data.lc 6:14-6:20  V1
+testdata/data.lc 6:33-6:34  'Data2->'Int
 testdata/data.lc 6:23-6:24  'Data2->'Int
+testdata/data.lc 7:14-7:20  'Int->V1
+testdata/data.lc 7:14-7:20  V1
+testdata/data.lc 7:14-7:20  'Int
+testdata/data.lc 7:23-7:24  'Data2->'Int
 testdata/data.lc 10:6-10:11  Type -> Type -> Type->Type
 testdata/data.lc 10:6-10:38  Type
 testdata/data.lc 10:36-10:38  Type
@@ -43,13 +58,26 @@ testdata/data.lc 12:37-12:42  Type
 testdata/data.lc 12:43-12:45  Type
 testdata/data.lc 12:46-12:48  Type
 testdata/data.lc 12:23-12:29  {a} -> {b} -> {c} -> 'Int -> a -> 'Float -> b -> c -> 'Data5 a b c
+testdata/data.lc 10:6-12:29  Type
+testdata/data.lc 10:23-10:29  Type
+testdata/data.lc 10:23-10:29  'Data5 V4 V3 V2
+testdata/data.lc 11:23-11:29  Type
+testdata/data.lc 11:23-11:29  'Data5 V7 V6 V5
+testdata/data.lc 12:23-12:29  Type
+testdata/data.lc 12:23-12:29  'Data5 V10 V9 V8
+testdata/data.lc 10:23-10:29  V3->V1
+testdata/data.lc 10:23-10:29  V1
+testdata/data.lc 10:23-10:29  V4
+testdata/data.lc 10:23-10:29  'Data5 V2 V1 V0
+testdata/data.lc 10:32-10:34  {a} -> {b} -> {c} -> 'Data5 a b c -> a
 testdata/data.lc 11:23-11:29  V3 -> V3 -> V3->V3
 testdata/data.lc 11:23-11:29  V3 -> V3->V3
 testdata/data.lc 11:23-11:29  V3->V3
 testdata/data.lc 11:23-11:29  V3
-testdata/data.lc 11:23-11:29  V5
-testdata/data.lc 11:23-11:29  'Data5 V2 V1 V0
 testdata/data.lc 11:23-11:29  V4
+testdata/data.lc 11:23-11:29  'Data5 V2 V1 V0
+testdata/data.lc 11:48-11:50  {a} -> {b} -> {c} -> 'Data5 a b c -> c
+testdata/data.lc 11:23-11:29  V5
 testdata/data.lc 11:40-11:42  {a} -> {b} -> {c} -> 'Data5 a b c -> b
 testdata/data.lc 11:23-11:29  V6
 testdata/data.lc 11:32-11:34  {a} -> {b} -> {c} -> 'Data5 a b c -> a
diff --git a/testdata/language-features/basic-values/data01.out b/testdata/language-features/basic-values/data01.out
index e575c0c6..3507b1ab 100644
--- a/testdata/language-features/basic-values/data01.out
+++ b/testdata/language-features/basic-values/data01.out
@@ -4,13 +4,20 @@ testdata/language-features/basic-values/data01.lc 1:6-1:7  Type
 testdata/language-features/basic-values/data01.lc 1:8-1:9  'A
 testdata/language-features/basic-values/data01.lc 1:10-1:11  'A
 testdata/language-features/basic-values/data01.lc 1:12-1:13  'A
+testdata/language-features/basic-values/data01.lc 1:6-1:13  Type
 testdata/language-features/basic-values/data01.lc 3:6-3:7  Type
 testdata/language-features/basic-values/data01.lc 3:10-3:11  'E
 testdata/language-features/basic-values/data01.lc 3:16-3:18  Type
 testdata/language-features/basic-values/data01.lc 3:14-3:15  'Tuple0->'E
 testdata/language-features/basic-values/data01.lc 3:21-3:22  'E
+testdata/language-features/basic-values/data01.lc 3:6-3:22  Type
+testdata/language-features/basic-values/data01.lc 3:14-3:15  Type
+testdata/language-features/basic-values/data01.lc 3:14-3:15  'E
 testdata/language-features/basic-values/data01.lc 5:6-5:8  Type
 testdata/language-features/basic-values/data01.lc 5:9-5:11  'D1
 testdata/language-features/basic-values/data01.lc 6:7-6:9  Type
 testdata/language-features/basic-values/data01.lc 6:5-6:7  'Tuple0->'D1
 testdata/language-features/basic-values/data01.lc 6:11-6:13  'D1
+testdata/language-features/basic-values/data01.lc 5:6-6:13  Type
+testdata/language-features/basic-values/data01.lc 6:5-6:7  Type
+testdata/language-features/basic-values/data01.lc 6:5-6:7  'D1
diff --git a/testdata/traceTest.out b/testdata/traceTest.out
index adbb4fa4..16b64fc4 100644
--- a/testdata/traceTest.out
+++ b/testdata/traceTest.out
@@ -4,6 +4,8 @@ testdata/traceTest.lc 6:8-6:9  V1
 testdata/traceTest.lc 6:1-6:3  {a} -> a->a
 testdata/traceTest.lc 8:17-8:18  Type
 testdata/traceTest.lc 8:6-8:7  {a} -> a->Type
+testdata/traceTest.lc 8:6-8:18  Type
+testdata/traceTest.lc 8:6-8:7  Type
 testdata/traceTest.lc 10:6-10:24  Type
 testdata/traceTest.lc 10:6-10:7  {a} -> a->Type
 testdata/traceTest.lc 10:9-10:24  V0
diff --git a/testdata/typeclass.out b/testdata/typeclass.out
index 48d87905..d4817d5c 100644
--- a/testdata/typeclass.out
+++ b/testdata/typeclass.out
@@ -8,6 +8,10 @@ testdata/typeclass.lc 4:26-4:27  Type
 testdata/typeclass.lc 4:29-4:33  Type->Type
 testdata/typeclass.lc 4:34-4:35  Type
 testdata/typeclass.lc 4:21-4:25  {a} -> a -> 'List a -> 'List a
+testdata/typeclass.lc 4:6-4:25  Type
+testdata/typeclass.lc 4:15-4:18  'List V1
+testdata/typeclass.lc 4:21-4:25  Type
+testdata/typeclass.lc 4:21-4:25  'List V4
 testdata/typeclass.lc 11:13-11:17  V0
 testdata/typeclass.lc 11:13-11:17  'Bool
 testdata/typeclass.lc 10:12-10:17  'Bool