7 files changed, 169 insertions, 151 deletions

diff --git a/TODO b/TODO
index f676e203..2992a1a7 100644
--- a/TODO
+++ b/TODO
@@ -69,6 +69,11 @@ done:
 
 0.5  goal: improvement + linear time interpretation
 
+done:
+- compiler: (~) :: forall a . a -> a -> Type
+
+next:
+
 - blog about release:
   - few sentences about the past events
     - this is the 2nd version (first rewrite) of the DSL using the learnings from the first one
@@ -89,7 +94,6 @@ done:
 - docs: feature teaser, 2 min paper videos
 - testenv: performance benchmarks
 
-- compiler: (~) :: forall a b . a -> b -> Type
 - compiler: ConName --> Int
 - compiler: support let labels
 - compiler optimization: irrelevance + erasure
@@ -159,6 +163,7 @@ extra (refactoring):
 - community: blog about compiler internals
 - backend: generated backends
 - user supplied cpu values like color values and rendering context
+- compiler: (~) :: forall a b . a -> b -> Type   ?
 - compiler: add more structure to witnesses?
 - review all old disabled test cases
 - 100% test coverage of the parser
diff --git a/lc/Builtins.lc b/lc/Builtins.lc
index 77027a39..d4226f25 100644
--- a/lc/Builtins.lc
+++ b/lc/Builtins.lc
@@ -462,7 +462,7 @@ PrimBShiftL, PrimBShiftR      :: (Integral t, a ~ VecScalar d t, b ~ VecScalar d
 PrimBShiftLS, PrimBShiftRS    :: (Integral t, a ~ VecScalar d t) => a -> Word -> a
 -- Logic Functions
 PrimAnd, PrimOr, PrimXor      :: Bool -> Bool -> Bool
-PrimNot                       :: (a ~ VecScalar d Bool) => a -> a
+PrimNot                       :: forall a d . (a ~ VecScalar d Bool) => a -> a
 PrimAny, PrimAll              :: VecScalar d Bool -> Bool
 
 -- Angle, Trigonometry and Exponential Functions
@@ -509,8 +509,8 @@ PrimMulVecMat                 :: Vec h a   -> Mat h w a -> Vec w a
 PrimMulMatMat                 :: Mat i j a -> Mat j k a -> Mat i k a
 -- Vector and Scalar Relational Functions
 PrimLessThan, PrimLessThanEqual, PrimGreaterThan, PrimGreaterThanEqual, PrimEqualV, PrimNotEqualV
-                              :: (Num t, a ~ VecScalar d t, b ~ VecScalar d Bool) => a -> a -> b
-PrimEqual, PrimNotEqual       :: (t ~ MatVecScalarElem a) => a -> a -> Bool
+                              :: forall a d t b . (Num t, a ~ VecScalar d t, b ~ VecScalar d Bool) => a -> a -> b
+PrimEqual, PrimNotEqual       :: forall a t . (t ~ MatVecScalarElem a) => a -> a -> Bool
 -- Fragment Processing Functions
 PrimDFdx, PrimDFdy, PrimFWidth
                               :: (a ~ VecScalar d Float) => a -> a
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index 293b1bc9..04ce6ed1 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -892,7 +892,8 @@ toExp = flip runReader [] . flip evalStateT freshTypeVars . f_
             I.Pi b x yt -> newName >>= \n -> do
                 t <- f_ (x, I.TType)
                 Lam b (PVar t n) t <$> local ((Var n t, x):) (f_ (y, yt))
-        I.Con s n xs    -> Con (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) (I.mkConPars n et ++ xs)
+        I.Con s n xs    -> Con (show s) <$> f_ (t, I.TType) <*> chain [] t (I.mkConPars n et ++ xs)
+          where t = I.conType et s
         I.TyCon s xs    -> Con (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) xs
         I.Fun s xs      -> Fun (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) xs
         I.CaseFun s xs n -> asks makeTE >>= \te -> Fun (show s) <$> f_ (I.nType s, I.TType) <*> chain [] (I.nType s) (I.makeCaseFunPars te n ++ xs ++ [I.Neut n])
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index ae2a9f1b..21ffe022 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -26,7 +26,7 @@ module LambdaCube.Compiler.Infer
     , Infos(..), listInfos, ErrorMsg(..), PolyEnv(..), ErrorT, throwErrorTCM, parseLC, joinPolyEnvs, filterPolyEnv, inference_
     , ImportItems (..)
     , SI(..), Range(..)
-    , nType, neutType, appTy, mkConPars, makeCaseFunPars, unpmlabel
+    , nType, conType, neutType, appTy, mkConPars, makeCaseFunPars, unpmlabel
     , MaxDB(..)
     ) where
 import Data.Monoid
@@ -69,9 +69,9 @@ data Neutral
     | PMLabel_ FunName !Int [Exp] Exp{-unfolded expression-}
   deriving (Show)
 
-data ConName = ConName SName MFixity Int{-ordinal number, e.g. Zero:0, Succ:1-} TyConName Type
+data ConName = ConName SName MFixity Int{-ordinal number, e.g. Zero:0, Succ:1-} Type
 
-data TyConName = TyConName SName MFixity Int{-num of indices-} Type [ConName]{-constructors-} CaseFunName
+data TyConName = TyConName SName MFixity Int{-num of indices-} Type [(ConName, Type)]{-constructors-} CaseFunName
 
 data FunName = FunName_ SName ([Exp] -> Exp) MFixity Type
 pattern FunName a b c <- FunName_ a _ b c where FunName a b c = funName a b c
@@ -86,8 +86,8 @@ type Type = Exp
 type ExpType = (Exp, Type)
 type SExp2 = SExp' ExpType
 
-instance Show ConName where show (ConName n _ _ _ _) = n
-instance Eq ConName where ConName _ _ n _ _ == ConName _ _ n' _ _ = n == n'
+instance Show ConName where show (ConName n _ _ _) = n
+instance Eq ConName where ConName _ _ n _ == ConName _ _ n' _ = n == n'
 instance Show TyConName where show (TyConName n _ _ _ _ _) = n
 instance Eq TyConName where TyConName n _ _ _ _ _ == TyConName n' _ _ _ _ _ = n == n'
 instance Show FunName where show (FunName n _ _) = n
@@ -115,9 +115,7 @@ pattern Var a = Neut (Var_ a)
 conParams (conTypeName -> TyConName _ _ _ _ _ (CaseFunName _ _ pars)) = pars
 mkConPars n (snd . getParams -> TyCon (TyConName _ _ _ _ _ (CaseFunName _ _ pars)) xs) = take (min n pars) xs
 mkConPars n x = error $ "mkConPars: " ++ ppShow x
-conName a b c d = ConName a b c (get $ snd $ getParams d) d
-  where
-    get (TyCon s _) = s
+conName = ConName
 
 makeCaseFunPars te n = case neutType te n of
     TyCon (TyConName _ _ _ _ _ (CaseFunName _ _ pars)) xs -> take pars xs
@@ -126,7 +124,8 @@ pattern Closed :: () => Up a => a -> a
 pattern Closed a <- a where Closed a = closedExp a
 
 pattern Con x n y <- Con_ _ x n y where Con x n y = Con_ (foldMap maxDB_ y) x n y
-pattern ConN s a  <- Con (ConName s _ _ _ _) _ a
+pattern ConN s a  <- Con (ConName s _ _ _) _ a
+pattern ConN' s a  <- Con (ConName _ _ s _) _ a
 tCon s i t a = Con (conName s Nothing i t) 0 a
 tCon_ k s i t a = Con (conName s Nothing i t) k a
 pattern TyCon x y <- TyCon_ _ x y where TyCon x y = TyCon_ (foldMap maxDB_ y) x y
@@ -136,26 +135,31 @@ pattern FunN a b <- Fun (FunName a _ _) b
 pattern TFun a t b <- Fun (FunName a _ t) b where TFun a t b = Fun (FunName a Nothing t) b
 pattern TFun' a t b <- Fun_ (FunName a _ t) b where TFun' a t b = Fun_ (FunName a Nothing t) b
 pattern TyConN s a <- TyCon (TyConName s _ _ _ _ _) a
-pattern TTyCon s t a <- TyCon (TyConName s _ _ t _ _) a where TTyCon s t a = TyCon (TyConName s Nothing (error "todo: inum") t (error "todo: tcn cons 2") $ CaseFunName (error "TTyCon-A") (error "TTyCon-B") $ length a) a
-pattern TTyCon0 s  <- TyCon (TyConName s _ _ TType _ _) [] where TTyCon0 s = Closed $ TyCon (TyConName s Nothing 0 TType (error "todo: tcn cons 3") $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) []
+pattern TTyCon s t a <- TyCon (TyConName s _ _ t _ _) a
+tTyCon s t a cs = TyCon (TyConName s Nothing (error "todo: inum") t (map ((,) (error "tTyCon")) cs) $ CaseFunName (error "TTyCon-A") (error "TTyCon-B") $ length a) a
+pattern TTyCon0 s  <- TyCon (TyConName s _ _ TType _ _) []
+tTyCon0 s cs = Closed $ TyCon (TyConName s Nothing 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) []
 pattern a :~> b = Pi Visible a b
 
-pattern Unit        = TTyCon0 "'Unit"
-pattern TInt        = TTyCon0 "'Int"
-pattern TImageSemantics        = TTyCon0 "'ImageSemantics"
-pattern TNat        = TTyCon0 "'Nat"
-pattern TBool       = TTyCon0 "'Bool"
-pattern TFloat      = TTyCon0 "'Float"
-pattern TString     = TTyCon0 "'String"
-pattern TChar       = TTyCon0 "'Char"
-pattern TOrdering   = TTyCon0 "'Ordering"
-pattern TTuple2 a b = TTyCon "'Tuple2" (TType :~> TType :~> TType) [a, b]
-pattern TVec a b   <- TyConN "'VecS" {-(TType :~> TNat :~> TType)-} [b, a]
-pattern TList a     = TTyCon "'List" (TType :~> TType) [a]
+pattern Unit        <- TTyCon0 "'Unit"      where Unit = tTyCon0 "'Unit" [Unit]
+pattern TInt        <- TTyCon0 "'Int"       where TInt = tTyCon0 "'Int" $ error "cs 1"
+pattern TImageSemantics <- TTyCon0 "'ImageSemantics" where TImageSemantics = tTyCon0 "'ImageSemantics" $ error "cs 2"
+pattern TNat        <- TTyCon0 "'Nat"       where TNat = tTyCon0 "'Nat" $ error "cs 3"
+pattern TBool       <- TTyCon0 "'Bool"      where TBool = tTyCon0 "'Bool" $ error "cs 4"
+pattern TFloat      <- TTyCon0 "'Float"     where TFloat = tTyCon0 "'Float" $ error "cs 5"
+pattern TString     <- TTyCon0 "'String"    where TString = tTyCon0 "'String" $ error "cs 6"
+pattern TChar       <- TTyCon0 "'Char"      where TChar = tTyCon0 "'Char" $ error "cs 7"
+pattern TOrdering   <- TTyCon0 "'Ordering"  where TOrdering = tTyCon0 "'Ordering" $ error "cs 8"
+pattern TOutput     <- TTyCon0 "'Output"    where TOutput = tTyCon0 "'Output" $ error "cs 9"
+pattern TTuple0     <- TTyCon0 "'Tuple0"    where TTuple0 = tTyCon0 "'Tuple0" $ error "cs 10"
+pattern TVec a b    <- TyConN "'VecS" {-(TType :~> TNat :~> TType)-} [b, a]
+--pattern TTuple2 a b = TTyCon "'Tuple2" (TType :~> TType :~> TType) [a, b]
+pattern TList a     <- TyConN "'List" [a] where TList a = tTyCon "'List" (TType :~> TType) [a] $ error "cs 11"
+pattern TInterpolated x <- TyConN "'Interpolated" [x] where TInterpolated x = tTyCon "'Interpolated" (TType :~> TType) [x] $ error "cs 12"
 pattern Empty s   <- TyCon (TyConName "'Empty" _ _ _ _ _) [EString s] where
         Empty s    = TyCon (TyConName "'Empty" Nothing (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [EString s]
 
-pattern TT          <- ConN "TT" _ where TT = Closed (tCon "TT" 0 Unit [])
+pattern TT          <- ConN' _ _ where TT = Closed (tCon "TT" 0 Unit [])
 nil                 = (tCon_ 1 "Nil" 0 (Pi Hidden TType $ TList (Var 0)) [])
 cons a b            = (tCon_ 1 "Cons" 1 (Pi Hidden TType $ Var 0 :~> TList (Var 1) :~> TList (Var 2)) [a, b])
 pattern Zero        <- ConN "Zero" _ where Zero = Closed (tCon "Zero" 0 TNat [])
@@ -177,6 +181,7 @@ pattern EChar a     = ELit (LChar a)
 pattern EString a   = ELit (LString a)
 pattern EBool a <- (getEBool -> Just a) where EBool = mkBool
 pattern ENat n <- (fromNatE -> Just n) where ENat = toNatE
+pattern ENat' n <- (fromNatE' -> Just n)
 
 pattern NoTup <- (noTup -> True)
 
@@ -191,19 +196,24 @@ pattern NoTup <- (noTup -> True)
 --tTuple3 a b c = TTyCon "'Tuple3" (TType :~> TType :~> TType :~> TType) [a, b, c]
 
 toNatE :: Int -> Exp
-toNatE 0         = Closed Zero
+toNatE 0         = Zero
 toNatE n | n > 0 = Closed (Succ (toNatE (n - 1)))
 
 fromNatE :: Exp -> Maybe Int
-fromNatE Zero = Just 0
-fromNatE (Succ n) = (1 +) <$> fromNatE n
+fromNatE (ConN' 0 _) = Just 0
+fromNatE (ConN' 1 [n]) = (1 +) <$> fromNatE n
 fromNatE _ = Nothing
 
+fromNatE' :: Exp -> Maybe Int
+fromNatE' Zero = Just 0
+fromNatE' (Succ n) = (1 +) <$> fromNatE' n
+fromNatE' _ = Nothing
+
 mkBool False = Closed $ tCon "False" 0 TBool []
 mkBool True  = Closed $ tCon "True"  1 TBool []
 
-getEBool (ConN "False" _) = Just False
-getEBool (ConN "True" _) = Just True
+getEBool (ConN' 0 _) = Just False
+getEBool (ConN' 1 _) = Just True
 getEBool _ = Nothing
 
 mkOrdering x = Closed $ case x of
@@ -215,9 +225,9 @@ noTup (TyConN s _) = take 6 s /= "'Tuple" -- todo
 noTup _ = False
 
 conTypeName :: ConName -> TyConName
-conTypeName (ConName _ _ _ t _) = t
+conTypeName (ConName _ _ _ t) = case snd $ getParams t of TyCon n _ -> n
 
-outputType = TTyCon0 "'Output"
+outputType = TOutput
 boolType = TBool
 trueExp = EBool True
 
@@ -427,7 +437,7 @@ varType err n_ env = f n_ env where
     f n e = either (error $ "varType: " ++ err ++ "\n" ++ show n_ ++ "\n" ++ ppShow env) (f n) $ parent e
 
 -------------------------------------------------------------------------------- reduction
-evalCaseFun a ps (Con n@(ConName _ _ i _ _) _ vs)
+evalCaseFun a ps (Con n@(ConName _ _ i _) _ vs)
     | i /= (-1) = foldl app_ (ps !!! (i + 1)) vs
     | otherwise = error "evcf"
   where
@@ -485,14 +495,14 @@ getFunDef s = case show s of
     "primCompareString" -> \case [EString x, EString y] -> mkOrdering $ x `compare` y; xs -> f xs
 
     -- LambdaCube 3D specific primitives
-    "PrimGreaterThan" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (>) x y -> r; xs -> f xs
-    "PrimGreaterThanEqual" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (>=) x y -> r; xs -> f xs
-    "PrimLessThan" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (<) x y -> r; xs -> f xs
-    "PrimLessThanEqual" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (<=) x y -> r; xs -> f xs
-    "PrimEqualV" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (==) x y -> r; xs -> f xs
-    "PrimNotEqualV" -> \case [_, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (/=) x y -> r; xs -> f xs
-    "PrimEqual" -> \case [_, _, _, x, y] | Just r <- twoOpBool (==) x y -> r; xs -> f xs
-    "PrimNotEqual" -> \case [_, _, _, x, y] | Just r <- twoOpBool (/=) x y -> r; xs -> f xs
+    "PrimGreaterThan" -> \case [t, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (>) t x y -> r; xs -> f xs
+    "PrimGreaterThanEqual" -> \case [t, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (>=) t x y -> r; xs -> f xs
+    "PrimLessThan" -> \case [t, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (<) t x y -> r; xs -> f xs
+    "PrimLessThanEqual" -> \case [t, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (<=) t x y -> r; xs -> f xs
+    "PrimEqualV" -> \case [t, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (==) t x y -> r; xs -> f xs
+    "PrimNotEqualV" -> \case [t, _, _, _, _, _, _, x, y] | Just r <- twoOpBool (/=) t x y -> r; xs -> f xs
+    "PrimEqual" -> \case [t, _, _, x, y] | Just r <- twoOpBool (==) t x y -> r; xs -> f xs
+    "PrimNotEqual" -> \case [t, _, _, x, y] | Just r <- twoOpBool (/=) t x y -> r; xs -> f xs
     "PrimSubS" -> \case [_, _, _, _, x, y] | Just r <- twoOp (-) x y -> r; xs -> f xs
     "PrimSub" -> \case [_, _, x, y] | Just r <- twoOp (-) x y -> r; xs -> f xs
     "PrimAddS" -> \case [_, _, _, _, x, y] | Just r <- twoOp (+) x y -> r; xs -> f xs
@@ -507,7 +517,7 @@ getFunDef s = case show s of
     "PrimAnd" -> \case [EBool x, EBool y] -> EBool (x && y); xs -> f xs
     "PrimOr" -> \case [EBool x, EBool y] -> EBool (x || y); xs -> f xs
     "PrimXor" -> \case [EBool x, EBool y] -> EBool (x /= y); xs -> f xs
-    "PrimNot" -> \case [_, _, _, EBool x] -> EBool $ not x; xs -> f xs
+    "PrimNot" -> \case [TNat, _, _, EBool x] -> EBool $ not x; xs -> f xs
 
     _ -> f
   where
@@ -521,7 +531,7 @@ cstr = f []
     f ns typ (FixLabel _ a) a' = f ns typ a a'
     f ns typ a (FixLabel _ a') = f ns typ a a'
     f ns typ (Con a n xs) (Con a' n' xs') | a == a' && n == n' && length xs == length xs' = 
-        if null xs then Unit else ff ns (foldl appTy (nType a) $ mkConPars n typ) $ zip xs xs'
+        if null xs then Unit else ff ns (foldl appTy (conType typ a) $ mkConPars n typ) $ zip xs xs'
     f ns typ (TyCon a xs) (TyCon a' xs') | a == a' && length xs == length xs' = 
         ff ns (nType a) $ zip xs xs'
     f (_: ns) typ{-down?-} (down 0 -> Just a) (down 0 -> Just a') = f ns typ a a'
@@ -537,9 +547,9 @@ cstr = f []
 
     f ns@[] TType (TyConN "'Tuple2" [x, y]) (UFunN "'JoinTupleType" [x', y']) = t2 (f ns TType x x') (f ns TType y y')
     f ns@[] TType (UFunN "'JoinTupleType" [x', y']) (TyConN "'Tuple2" [x, y]) = t2 (f ns TType x' x) (f ns TType y' y)
-    f ns@[] TType (UFunN "'JoinTupleType" [x', y']) x@NoTup  = t2 (f ns TType x' x) (f ns TType y' $ TTyCon0 "'Tuple0")
+    f ns@[] TType (UFunN "'JoinTupleType" [x', y']) x@NoTup  = t2 (f ns TType x' x) (f ns TType y' TTuple0)
 
-    f ns@[] TType (x@NoTup) (UFunN "'InterpolatedType" [x']) = f ns TType (TTyCon "'Interpolated" (TType :~> TType) [x]) x'
+    f ns@[] TType (x@NoTup) (UFunN "'InterpolatedType" [x']) = f ns TType (TInterpolated x) x'
 
     f [] typ a@Neut{} a' = CstrT typ a a'
     f [] typ a a'@Neut{} = CstrT typ a a'
@@ -593,13 +603,13 @@ twoOp_ _ _ _ _ = Nothing
 
 modF x y = x - fromIntegral (floor (x / y)) * y
 
-twoOpBool :: (forall a . Ord a => a -> a -> Bool) -> Exp -> Exp -> Maybe Exp
-twoOpBool f (EFloat x)  (EFloat y)  = Just $ EBool $ f x y
-twoOpBool f (EInt x)    (EInt y)    = Just $ EBool $ f x y
-twoOpBool f (EString x) (EString y) = Just $ EBool $ f x y
-twoOpBool f (EChar x)   (EChar y)   = Just $ EBool $ f x y
-twoOpBool f (ENat x)    (ENat y)    = Just $ EBool $ f x y
-twoOpBool _ _ _ = Nothing
+twoOpBool :: (forall a . Ord a => a -> a -> Bool) -> Exp -> Exp -> Exp -> Maybe Exp
+twoOpBool f t (EFloat x)  (EFloat y)  = Just $ EBool $ f x y
+twoOpBool f t (EInt x)    (EInt y)    = Just $ EBool $ f x y
+twoOpBool f t (EString x) (EString y) = Just $ EBool $ f x y
+twoOpBool f t (EChar x)   (EChar y)   = Just $ EBool $ f x y
+twoOpBool f TNat (ENat x)    (ENat y)    = Just $ EBool $ f x y
+twoOpBool _ _ _ _ = Nothing
 
 app_ :: Exp -> Exp -> Exp
 app_ (Lam x) a = subst 0 a x
@@ -705,11 +715,13 @@ litType = \case
 class NType a where nType :: a -> Type
 
 instance NType FunName where nType (FunName _ _ t) = t
-instance NType ConName where nType (ConName _ _ _ _ t) = t
+--instance NType ConName where nType (ConName _ _ _ t) = t
 instance NType TyConName where nType (TyConName _ _ _ t _ _) = t
 instance NType CaseFunName where nType (CaseFunName _ t _) = t
 instance NType TyCaseFunName where nType (TyCaseFunName _ t) = t
 
+conType (snd . getParams -> TyCon (TyConName _ _ _ _ cs _) _) (ConName _ _ n t) = t -- snd $ cs !! n
+
 neutType te = \case
     App_ f x        -> appTy (neutType te f) x
     Var_ i          -> snd $ varType "C" i te
@@ -962,7 +974,7 @@ recheck' msg' e (x, xt) = (recheck_ "main" (checkEnv e) (x, xt), xt)
         (Neut (App_ a b), zt)
             | (Neut a', at) <- recheck'' "app1" te (Neut a, neutType te a)
             -> checkApps "a" [] zt (Neut . App_ a' . head) te at [b]
-        (Con s n as, zt)      -> checkApps (show s) [] zt (Con s n . drop (conParams s)) te (nType s) $ mkConPars n zt ++ as
+        (Con s n as, zt)      -> checkApps (show s) [] zt (Con s n . drop (conParams s)) te (conType zt s) $ mkConPars n zt ++ as
         (TyCon s as, zt)      -> checkApps (show s) [] zt (TyCon s) te (nType s) as
         (Fun s as, zt)        -> checkApps (show s ++ ppShow as ++ ppShow (nType s)) [] zt (Fun s) te (nType s) as
         (CaseFun s@(CaseFunName _ t pars) as n, zt) -> checkApps (show s) [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n])
@@ -1049,7 +1061,7 @@ extractDesugarInfo :: GlobalEnv -> DesugarInfo
 extractDesugarInfo ge =
     ( Map.fromList
         [ (n, f) | (n, (d, _, si)) <- Map.toList ge, f <- maybeToList $ case d of
-            Con (ConName _ f _ _ _) 0 [] -> f
+            Con (ConName _ f _ _) 0 [] -> f
             TyCon (TyConName _ f _ _ _ _) [] -> f
             (getLams -> (Fun (FunName _ f _) [])) -> f
             PMLabel (FunName _ f _) _ [] _ -> f
@@ -1065,7 +1077,7 @@ extractDesugarInfo ge =
         ]
     )
   where
-    f (ConName n _ _ _ ct) = (n, pars ct)
+    f (ConName n _ _ _, ct) = (n, pars ct)
     pars = length . filter ((==Visible) . fst) . fst . getParams
 
 -------------------------------------------------------------------------------- infos
@@ -1116,7 +1128,7 @@ handleStmt defs = \case
                         acts = map fst . fst . getParams $ cty
                         conn = conName (snd cn) (listToMaybe [f | PrecDef n f <- defs, n == cn]) j cty
                 addToEnv cn (Con conn 0 [], cty)
-                return ( conn
+                return ( (conn, cty)
                        , addParamsS pars
                        $ foldl SAppV (SVar (debugSI "22", ".cs") $ j + length pars) $ drop pnum' xs ++ [apps' (SGlobal cn) (zip acts $ downToS (j+1+length pars) (length ps) ++ downToS 0 (act- length ps))]
                        )
@@ -1330,7 +1342,7 @@ instance MkDoc Exp where
 --            Lam h a b       -> join $ shLam (used 0 b) (BLam h) <$> f a <*> pure (f b)
             Lam b          -> join $ shLam True (BLam Visible) <$> f TType{-todo-} <*> pure (f b)
             Pi h a b        -> join $ shLam (used 0 b) (BPi h) <$> f a <*> pure (f b)
-            ENat n          -> pure $ shAtom $ show n
+            ENat' n         -> pure $ shAtom $ show n
             Con s _ xs      -> foldl (shApp Visible) (shAtom_ $ show s) <$> mapM f xs
             TyConN s xs     -> foldl (shApp Visible) (shAtom_ s) <$> mapM f xs
             TType           -> pure $ shAtom "Type"
diff --git a/testdata/Builtins.out b/testdata/Builtins.out
index a83047df..1735f193 100644
--- a/testdata/Builtins.out
+++ b/testdata/Builtins.out
@@ -1979,19 +1979,19 @@ testdata/Builtins.lc 464:42-464:46  Type
 testdata/Builtins.lc 464:42-464:54  Type
 testdata/Builtins.lc 464:50-464:54  Type
 testdata/Builtins.lc 465:1-465:8  {a} -> {b:Nat} -> {c : a ~ VecScalar b Bool} -> a->a
-testdata/Builtins.lc 465:34-465:56  Type
-testdata/Builtins.lc 465:34-465:66  Type
-testdata/Builtins.lc 465:35-465:36  V3
-testdata/Builtins.lc 465:35-465:38  Type->Type
-testdata/Builtins.lc 465:37-465:38  Type -> Type->Type
-testdata/Builtins.lc 465:39-465:48  Nat -> Type->Type
-testdata/Builtins.lc 465:39-465:50  Type->Type
-testdata/Builtins.lc 465:39-465:55  Type
-testdata/Builtins.lc 465:49-465:50  V1
-testdata/Builtins.lc 465:51-465:55  Type
-testdata/Builtins.lc 465:60-465:61  Type
-testdata/Builtins.lc 465:60-465:66  Type
-testdata/Builtins.lc 465:65-465:66  Type
+testdata/Builtins.lc 465:47-465:69  Type
+testdata/Builtins.lc 465:47-465:79  Type
+testdata/Builtins.lc 465:48-465:49  V3
+testdata/Builtins.lc 465:48-465:51  Type->Type
+testdata/Builtins.lc 465:50-465:51  Type -> Type->Type
+testdata/Builtins.lc 465:52-465:61  Nat -> Type->Type
+testdata/Builtins.lc 465:52-465:63  Type->Type
+testdata/Builtins.lc 465:52-465:68  Type
+testdata/Builtins.lc 465:62-465:63  V1
+testdata/Builtins.lc 465:64-465:68  Type
+testdata/Builtins.lc 465:73-465:74  Type
+testdata/Builtins.lc 465:73-465:79  Type
+testdata/Builtins.lc 465:78-465:79  Type
 testdata/Builtins.lc 466:1-466:8  {a:Nat} -> VecScalar a Bool -> Bool
 testdata/Builtins.lc 466:10-466:17  {a:Nat} -> VecScalar a Bool -> Bool
 testdata/Builtins.lc 466:34-466:43  Nat -> Type->Type
@@ -2618,56 +2618,56 @@ testdata/Builtins.lc 509:60-509:69  Type
 testdata/Builtins.lc 509:64-509:65  Nat
 testdata/Builtins.lc 509:66-509:67  Nat
 testdata/Builtins.lc 509:68-509:69  Type
-testdata/Builtins.lc 511:1-511:13  {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
-testdata/Builtins.lc 511:15-511:32  {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
-testdata/Builtins.lc 511:34-511:49  {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
-testdata/Builtins.lc 511:51-511:71  {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
-testdata/Builtins.lc 511:73-511:83  {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
-testdata/Builtins.lc 511:85-511:98  {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
-testdata/Builtins.lc 512:34-512:97  Type
-testdata/Builtins.lc 512:35-512:38  Type->Type
-testdata/Builtins.lc 512:35-512:40  Type
-testdata/Builtins.lc 512:39-512:40  V7
-testdata/Builtins.lc 512:42-512:43  V6
-testdata/Builtins.lc 512:42-512:45  Type->Type
-testdata/Builtins.lc 512:42-512:59  Type
-testdata/Builtins.lc 512:42-512:97  Type
-testdata/Builtins.lc 512:44-512:45  Type -> Type->Type
-testdata/Builtins.lc 512:46-512:55  Nat -> Type->Type
-testdata/Builtins.lc 512:46-512:57  Type->Type
-testdata/Builtins.lc 512:46-512:59  Type
-testdata/Builtins.lc 512:56-512:57  V4
-testdata/Builtins.lc 512:58-512:59  Type
-testdata/Builtins.lc 512:61-512:62  V3
-testdata/Builtins.lc 512:61-512:64  Type->Type
-testdata/Builtins.lc 512:61-512:81  Type
-testdata/Builtins.lc 512:61-512:97  Type
-testdata/Builtins.lc 512:63-512:64  Type -> Type->Type
-testdata/Builtins.lc 512:65-512:74  Nat -> Type->Type
-testdata/Builtins.lc 512:65-512:76  Type->Type
-testdata/Builtins.lc 512:65-512:81  Type
-testdata/Builtins.lc 512:75-512:76  Nat
-testdata/Builtins.lc 512:77-512:81  Type
-testdata/Builtins.lc 512:86-512:87  Type
-testdata/Builtins.lc 512:86-512:97  Type
-testdata/Builtins.lc 512:91-512:92  Type
-testdata/Builtins.lc 512:91-512:97  Type
-testdata/Builtins.lc 512:96-512:97  Type
-testdata/Builtins.lc 513:1-513:10  {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool
-testdata/Builtins.lc 513:12-513:24  {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool
-testdata/Builtins.lc 513:34-513:58  Type
-testdata/Builtins.lc 513:34-513:76  Type
-testdata/Builtins.lc 513:35-513:36  V3
-testdata/Builtins.lc 513:35-513:38  Type->Type
-testdata/Builtins.lc 513:37-513:38  Type -> Type->Type
-testdata/Builtins.lc 513:39-513:55  Type->Type
-testdata/Builtins.lc 513:39-513:57  Type
-testdata/Builtins.lc 513:56-513:57  V1
-testdata/Builtins.lc 513:62-513:63  Type
-testdata/Builtins.lc 513:62-513:76  Type
-testdata/Builtins.lc 513:67-513:68  Type
-testdata/Builtins.lc 513:67-513:76  Type
-testdata/Builtins.lc 513:72-513:76  Type
+testdata/Builtins.lc 511:1-511:13  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
+testdata/Builtins.lc 511:15-511:32  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
+testdata/Builtins.lc 511:34-511:49  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
+testdata/Builtins.lc 511:51-511:71  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
+testdata/Builtins.lc 511:73-511:83  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
+testdata/Builtins.lc 511:85-511:98  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
+testdata/Builtins.lc 512:51-512:114  Type
+testdata/Builtins.lc 512:52-512:55  Type->Type
+testdata/Builtins.lc 512:52-512:57  Type
+testdata/Builtins.lc 512:56-512:57  V3
+testdata/Builtins.lc 512:59-512:60  V7
+testdata/Builtins.lc 512:59-512:62  Type->Type
+testdata/Builtins.lc 512:59-512:76  Type
+testdata/Builtins.lc 512:59-512:114  Type
+testdata/Builtins.lc 512:61-512:62  Type -> Type->Type
+testdata/Builtins.lc 512:63-512:72  Nat -> Type->Type
+testdata/Builtins.lc 512:63-512:74  Type->Type
+testdata/Builtins.lc 512:63-512:76  Type
+testdata/Builtins.lc 512:73-512:74  V5
+testdata/Builtins.lc 512:75-512:76  Type
+testdata/Builtins.lc 512:78-512:79  V3
+testdata/Builtins.lc 512:78-512:81  Type->Type
+testdata/Builtins.lc 512:78-512:98  Type
+testdata/Builtins.lc 512:78-512:114  Type
+testdata/Builtins.lc 512:80-512:81  Type -> Type->Type
+testdata/Builtins.lc 512:82-512:91  Nat -> Type->Type
+testdata/Builtins.lc 512:82-512:93  Type->Type
+testdata/Builtins.lc 512:82-512:98  Type
+testdata/Builtins.lc 512:92-512:93  Nat
+testdata/Builtins.lc 512:94-512:98  Type
+testdata/Builtins.lc 512:103-512:104  Type
+testdata/Builtins.lc 512:103-512:114  Type
+testdata/Builtins.lc 512:108-512:109  Type
+testdata/Builtins.lc 512:108-512:114  Type
+testdata/Builtins.lc 512:113-512:114  Type
+testdata/Builtins.lc 513:1-513:10  {a} -> {b} -> {c : b ~ MatVecScalarElem a} -> a -> a->Bool
+testdata/Builtins.lc 513:12-513:24  {a} -> {b} -> {c : b ~ MatVecScalarElem a} -> a -> a->Bool
+testdata/Builtins.lc 513:47-513:71  Type
+testdata/Builtins.lc 513:47-513:89  Type
+testdata/Builtins.lc 513:48-513:49  V1
+testdata/Builtins.lc 513:48-513:51  Type->Type
+testdata/Builtins.lc 513:50-513:51  Type -> Type->Type
+testdata/Builtins.lc 513:52-513:68  Type->Type
+testdata/Builtins.lc 513:52-513:70  Type
+testdata/Builtins.lc 513:69-513:70  V2
+testdata/Builtins.lc 513:75-513:76  Type
+testdata/Builtins.lc 513:75-513:89  Type
+testdata/Builtins.lc 513:80-513:81  Type
+testdata/Builtins.lc 513:80-513:89  Type
+testdata/Builtins.lc 513:85-513:89  Type
 testdata/Builtins.lc 515:1-515:9  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
 testdata/Builtins.lc 515:11-515:19  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
 testdata/Builtins.lc 515:21-515:31  {a} -> {b:Nat} -> {c : a ~ VecScalar b Float} -> a->a
diff --git a/testdata/Prelude.out b/testdata/Prelude.out
index 7dc75db8..b741d271 100644
--- a/testdata/Prelude.out
+++ b/testdata/Prelude.out
@@ -753,33 +753,33 @@ testdata/Prelude.lc 269:9-269:16  {a} -> {b : Signed (MatVecScalarElem a)} -> a-
 testdata/Prelude.lc 269:9-269:18  V2
 testdata/Prelude.lc 269:17-269:18  V3
 testdata/Prelude.lc 273:3-273:5  {a} -> a -> a->Bool
-testdata/Prelude.lc 273:10-273:22  {a} -> {b} -> {c : a ~ MatVecScalarElem b} -> b -> b->Bool
+testdata/Prelude.lc 273:10-273:22  {a} -> {b} -> {c : b ~ MatVecScalarElem a} -> a -> a->Bool
 testdata/Prelude.lc 273:10-273:24  V3->Bool
 testdata/Prelude.lc 273:10-273:26  Bool
 testdata/Prelude.lc 273:23-273:24  V4
 testdata/Prelude.lc 273:25-273:26  V1
-testdata/Prelude.lc 274:3-274:4  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
-testdata/Prelude.lc 274:9-274:21  {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
-testdata/Prelude.lc 274:9-274:23  VecScalar V1 V2 -> VecScalar V2 Bool
-testdata/Prelude.lc 274:9-274:25  VecScalar V1 Bool
+testdata/Prelude.lc 274:3-274:4  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
+testdata/Prelude.lc 274:9-274:21  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
+testdata/Prelude.lc 274:9-274:23  VecScalar V2 V1 -> VecScalar V3 Bool
+testdata/Prelude.lc 274:9-274:25  VecScalar V2 Bool
 testdata/Prelude.lc 274:22-274:23  V6
 testdata/Prelude.lc 274:24-274:25  V4
-testdata/Prelude.lc 275:3-275:5  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
-testdata/Prelude.lc 275:10-275:27  {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
-testdata/Prelude.lc 275:10-275:29  VecScalar V1 V2 -> VecScalar V2 Bool
-testdata/Prelude.lc 275:10-275:31  VecScalar V1 Bool
+testdata/Prelude.lc 275:3-275:5  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
+testdata/Prelude.lc 275:10-275:27  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
+testdata/Prelude.lc 275:10-275:29  VecScalar V2 V1 -> VecScalar V3 Bool
+testdata/Prelude.lc 275:10-275:31  VecScalar V2 Bool
 testdata/Prelude.lc 275:28-275:29  V6
 testdata/Prelude.lc 275:30-275:31  V4
-testdata/Prelude.lc 276:3-276:5  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
-testdata/Prelude.lc 276:10-276:30  {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
-testdata/Prelude.lc 276:10-276:32  VecScalar V1 V2 -> VecScalar V2 Bool
-testdata/Prelude.lc 276:10-276:34  VecScalar V1 Bool
+testdata/Prelude.lc 276:3-276:5  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
+testdata/Prelude.lc 276:10-276:30  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
+testdata/Prelude.lc 276:10-276:32  VecScalar V2 V1 -> VecScalar V3 Bool
+testdata/Prelude.lc 276:10-276:34  VecScalar V2 Bool
 testdata/Prelude.lc 276:31-276:32  V6
 testdata/Prelude.lc 276:33-276:34  V4
-testdata/Prelude.lc 277:3-277:4  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
-testdata/Prelude.lc 277:9-277:24  {a} -> {b} -> {c:Nat} -> {d} -> {e : Num a} -> {f : b ~ VecScalar c a} -> {g : d ~ VecScalar c Bool} -> b -> b->d
-testdata/Prelude.lc 277:9-277:26  VecScalar V1 V2 -> VecScalar V2 Bool
-testdata/Prelude.lc 277:9-277:28  VecScalar V1 Bool
+testdata/Prelude.lc 277:3-277:4  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
+testdata/Prelude.lc 277:9-277:24  {a} -> {b:Nat} -> {c} -> {d} -> {e : Num c} -> {f : a ~ VecScalar b c} -> {g : d ~ VecScalar b Bool} -> a -> a->d
+testdata/Prelude.lc 277:9-277:26  VecScalar V2 V1 -> VecScalar V3 Bool
+testdata/Prelude.lc 277:9-277:28  VecScalar V2 Bool
 testdata/Prelude.lc 277:25-277:26  V6
 testdata/Prelude.lc 277:27-277:28  V4
 testdata/Prelude.lc 280:3-280:5  Bool -> Bool->Bool
@@ -1048,7 +1048,7 @@ testdata/Prelude.lc 358:17-358:18  Float
 testdata/Prelude.lc 358:17-358:20  Float->Bool
 testdata/Prelude.lc 358:17-358:22  Bool
 testdata/Prelude.lc 358:17-358:30  List V0 -> List V1
-testdata/Prelude.lc 358:19-358:20  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
+testdata/Prelude.lc 358:19-358:20  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/Prelude.lc 358:21-358:22  Float
 testdata/Prelude.lc 358:28-358:30  {a} -> List a
 testdata/Prelude.lc 358:36-358:37  Float
diff --git a/testdata/complex.out b/testdata/complex.out
index 608be18c..444cab15 100644
--- a/testdata/complex.out
+++ b/testdata/complex.out
@@ -92,7 +92,7 @@ testdata/complex.lc 24:11-24:12  Float
 testdata/complex.lc 24:11-24:14  Float->Bool
 testdata/complex.lc 24:11-24:19  Bool
 testdata/complex.lc 24:11-24:59  Complex 'Polar -> Complex 'Polar
-testdata/complex.lc 24:13-24:14  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
+testdata/complex.lc 24:13-24:14  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/complex.lc 24:16-24:19  Float
 testdata/complex.lc 24:37-24:42  Float -> Float -> Complex 'Polar
 testdata/complex.lc 24:37-24:44  Float -> Complex 'Polar
@@ -112,13 +112,13 @@ testdata/complex.lc 25:11-25:19  Bool
 testdata/complex.lc 25:11-25:22  Bool->Bool
 testdata/complex.lc 25:11-25:31  Bool
 testdata/complex.lc 25:11-25:64  Complex 'Polar -> Complex 'Polar
-testdata/complex.lc 25:13-25:14  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
+testdata/complex.lc 25:13-25:14  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/complex.lc 25:16-25:19  Float
 testdata/complex.lc 25:20-25:22  Bool -> Bool->Bool
 testdata/complex.lc 25:23-25:24  Float
 testdata/complex.lc 25:23-25:27  Float->Bool
 testdata/complex.lc 25:23-25:31  Bool
-testdata/complex.lc 25:25-25:27  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
+testdata/complex.lc 25:25-25:27  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/complex.lc 25:28-25:31  Float
 testdata/complex.lc 25:37-25:42  Float -> Float -> Complex 'Polar
 testdata/complex.lc 25:37-25:44  Float -> Complex 'Polar
@@ -142,13 +142,13 @@ testdata/complex.lc 26:11-26:19  Bool
 testdata/complex.lc 26:11-26:22  Bool->Bool
 testdata/complex.lc 26:11-26:31  Bool
 testdata/complex.lc 26:11-26:64  Complex 'Polar -> Complex 'Polar
-testdata/complex.lc 26:13-26:14  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
+testdata/complex.lc 26:13-26:14  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/complex.lc 26:16-26:19  Float
 testdata/complex.lc 26:20-26:22  Bool -> Bool->Bool
 testdata/complex.lc 26:23-26:24  Float
 testdata/complex.lc 26:23-26:26  Float->Bool
 testdata/complex.lc 26:23-26:31  Bool
-testdata/complex.lc 26:25-26:26  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
+testdata/complex.lc 26:25-26:26  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/complex.lc 26:28-26:31  Float
 testdata/complex.lc 26:37-26:42  Float -> Float -> Complex 'Polar
 testdata/complex.lc 26:37-26:44  Float -> Complex 'Polar
@@ -178,7 +178,7 @@ testdata/complex.lc 27:20-27:22  Bool -> Bool->Bool
 testdata/complex.lc 27:23-27:24  Float
 testdata/complex.lc 27:23-27:27  Float->Bool
 testdata/complex.lc 27:23-27:31  Bool
-testdata/complex.lc 27:25-27:27  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
+testdata/complex.lc 27:25-27:27  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/complex.lc 27:28-27:31  Float
 testdata/complex.lc 27:37-27:42  Float -> Float -> Complex 'Polar
 testdata/complex.lc 27:37-27:44  Float -> Complex 'Polar
@@ -202,7 +202,7 @@ testdata/complex.lc 28:20-28:22  Bool -> Bool->Bool
 testdata/complex.lc 28:23-28:24  Float
 testdata/complex.lc 28:23-28:26  Float->Bool
 testdata/complex.lc 28:23-28:31  Bool
-testdata/complex.lc 28:25-28:26  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
+testdata/complex.lc 28:25-28:26  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/complex.lc 28:28-28:31  Float
 testdata/complex.lc 28:37-28:42  Float -> Float -> Complex 'Polar
 testdata/complex.lc 28:37-28:44  Float -> Complex 'Polar
@@ -381,5 +381,5 @@ testdata/complex.lc 145:12-145:31  Bool
 testdata/complex.lc 145:17-145:25  Complex V0
 testdata/complex.lc 145:18-145:22  {a:Repr} -> Complex a -> Complex a
 testdata/complex.lc 145:23-145:24  V6
-testdata/complex.lc 145:26-145:27  {a} -> {b:Nat} -> {c : Num a} -> VecScalar b a -> VecScalar b a -> VecScalar b Bool
+testdata/complex.lc 145:26-145:27  {a:Nat} -> {b} -> {c : Num b} -> VecScalar a b -> VecScalar a b -> VecScalar a Bool
 testdata/complex.lc 145:28-145:31  Float