tuples are heterogeneous lists

5 files changed, 188 insertions, 208 deletions

diff --git a/src/LambdaCube/Compiler.hs b/src/LambdaCube/Compiler.hs
index fc9068cc..54013b74 100644
--- a/src/LambdaCube/Compiler.hs
+++ b/src/LambdaCube/Compiler.hs
@@ -28,7 +28,7 @@ import Data.List
 import Data.Function
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
-import Control.Monad.State
+import Control.Monad.State.Strict
 import Control.Monad.Reader
 import Control.Monad.Writer
 import Control.Monad.Except
@@ -47,7 +47,7 @@ import LambdaCube.IR as IR
 import LambdaCube.Compiler.Pretty hiding ((</>))
 import LambdaCube.Compiler.Parser (Module(..), Export(..), ImportItems (..), runDefParser, parseLC)
 import LambdaCube.Compiler.Lexer as Exported (Range(..))
-import LambdaCube.Compiler.Infer (PolyEnv(..), showError, joinPolyEnvs, filterPolyEnv, inference_, extractDesugarInfo)
+import LambdaCube.Compiler.Infer (PolyEnv(..), showError, joinPolyEnvs, filterPolyEnv, inference_)
 import LambdaCube.Compiler.Infer as Exported (Infos, listAllInfos, listTypeInfos, listTraceInfos, Exp, outputType, boolType, trueExp, unfixlabel)
 import LambdaCube.Compiler.CoreToIR
 
@@ -148,20 +148,20 @@ loadModule imp mname_ = do
             do
                 ms <- mapM loadModuleImports $ moduleImports e
                 x' <- {-trace ("loading " ++ fname) $-} do
-                    env@(PolyEnv ge _) <- joinPolyEnvs False ms
-                    defs <- MMT $ mapExceptT (return . runIdentity) $ runDefParser (extractDesugarInfo ge) $ definitions e
+                    env@(PolyEnv ge _ ds) <- joinPolyEnvs False ms
+                    defs <- MMT $ mapExceptT (return . runIdentity) $ runDefParser ds $ definitions e
                     srcs <- gets $ Map.mapMaybe (either (const Nothing) (Just . snd))
                     x <- MMT $ mapExceptT (lift . lift . mapWriterT (return . first (left $ showError (Map.insert fname src srcs)) . runIdentity)) $ inference_ env (extensions e) defs
                     case moduleExports e of
                             Nothing -> return x
                             Just es -> joinPolyEnvs False $ flip map es $ \exp -> case exp of
                                 ExportId (snd -> d) -> case  Map.lookup d $ getPolyEnv x of
-                                    Just def -> PolyEnv (Map.singleton d def) mempty
+                                    Just def -> PolyEnv (Map.singleton d def) mempty mempty{-TODO-}
                                     Nothing  -> error $ d ++ " is not defined"
                                 ExportModule (snd -> m) | m == mname -> x
                                 ExportModule m -> case [ ms
                                                        | ((m', is), ms) <- zip (moduleImports e) ms, m' == m] of
-                                    [PolyEnv x infos] -> PolyEnv x mempty   -- TODO
+                                    [PolyEnv x infos ds] -> PolyEnv x mempty{-TODO-} ds
                                     []  -> error $ "empty export list: " ++ show (fname, m, map fst $ moduleImports e, mname)
                                     _   -> error "export list: internal error"
                 modify $ Map.insert fname $ Right (x', src)
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index de7a7720..8c759ea4 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -131,7 +131,7 @@ getCommands backend e = case e of
                     }
                 return (i, input)
               where
-                input = compAttribute attrs
+                input = compInputType'' attrs
                 mergeSlot a b = a
                   { IR.slotUniforms = IR.slotUniforms a <> IR.slotUniforms b
                   , IR.slotStreams  = IR.slotStreams a <> IR.slotStreams b
@@ -202,12 +202,12 @@ getSemantics = compSemantics . frameBufferType . tyOf
 getFragFilter (A2 "map" (EtaPrim2 "filterFragment" p) x) = (Just p, x)
 getFragFilter x = (Nothing, x)
 
-getVertexShader (A2 "map" (EtaPrim2 "mapPrimitive" f@(etaRed -> Just (_, o))) x) = ((Just f, tyOf o), x)
+getVertexShader (A2 "map" (EtaPrim2 "mapPrimitive" f@(etaReds -> Just (_, o))) x) = ((Just f, tyOf o), x)
 --getVertexShader (A2 "map" (EtaPrim2 "mapPrimitive" f) x) = error $ "gff: " ++ show (case f of ExpTV x _ _ -> x) --ppShow (mapVal unFunc' f)
 --getVertexShader x = error $ "gf: " ++ ppShow x
 getVertexShader x = ((Nothing, getPrim' $ tyOf x), x)
 
-getFragmentShader (A2 "map" (EtaPrim2 "mapFragment" f@(etaRed -> Just (_, o))) x) = ((Just f, tyOf o), x)
+getFragmentShader (A2 "map" (EtaPrim2 "mapFragment" f@(etaReds -> Just (_, o))) x) = ((Just f, tyOf o), x)
 --getFragmentShader (A2 "map" (EtaPrim2 "mapFragment" f) x) = error $ "gff: " ++ ppShow f
 --getFragmentShader x = error $ "gf: " ++ ppShow x
 getFragmentShader x = ((Nothing, getPrim'' $ tyOf x), x)
@@ -222,10 +222,11 @@ compFrameBuffer = \case
   A1 "ColorImage" a -> IR.ClearImage IR.Color $ compValue a
   x -> error $ "compFrameBuffer " ++ ppShow x
 
-compSemantics = \case
-  A2 "Cons" a b -> compSemantic a: compSemantics b
-  A0 "Nil" -> []
-  x -> error $ "compSemantics: " ++ ppShow x
+compSemantics = map compSemantic . compList
+
+compList (A2 "Cons" a x) = a : compList x
+compList (A0 "Nil") = []
+compList x = error $ "compList: " ++ ppShow x
 
 compSemantic = \case
   A1 "Depth" _   -> IR.Depth
@@ -371,24 +372,23 @@ compInputType_ x = case x of
   TMat 4 2 TFloat -> Just IR.M42F
   TMat 4 3 TFloat -> Just IR.M43F
   TMat 4 4 TFloat -> Just IR.M44F
+  -- hack
+  A1 "HList" (compList -> [x]) -> compInputType_ x
   _ -> Nothing
 
 compInputType msg x = fromMaybe (error $ "compInputType " ++ msg ++ " " ++ ppShow x) $ compInputType_ x
 
 is234 = (`elem` [2,3,4])
 
+compInputType'' attrs@(A1 "Attribute" (EString s)) | A1 "HList" (compList -> [ty]) <- tyOf attrs = [(s, compInputType "cit" ty)]
+compInputType'' attrs = map compAttribute $ eTuple attrs
 
-compAttribute x = case x of
-  ETuple a -> concatMap compAttribute a
-  A1 "Attribute" (EString s) -> [(s, compInputType "compAttr" $ tyOf x)]
+compAttribute = \case
+  x@(A1 "Attribute" (EString s)) -> (s, compInputType "compAttr" $ tyOf x)
   x -> error $ "compAttribute " ++ ppShow x
 
-compList (A2 "Cons" a x) = compValue a : compList x
-compList (A0 "Nil") = []
-compList x = error $ "compList: " ++ ppShow x
-
 compAttributeValue :: ExpTV -> [(IR.InputType,IR.ArrayValue)]
-compAttributeValue x = checkLength $ go x
+compAttributeValue x = checkLength $ map go $ eTuple x
   where
     emptyArray t | t `elem` [IR.Float,IR.V2F,IR.V3F,IR.V4F,IR.M22F,IR.M23F,IR.M24F,IR.M32F,IR.M33F,IR.M34F,IR.M42F,IR.M43F,IR.M44F] = IR.VFloatArray mempty
     emptyArray t | t `elem` [IR.Int,IR.V2I,IR.V3I,IR.V4I] = IR.VIntArray mempty
@@ -406,12 +406,9 @@ compAttributeValue x = checkLength $ go x
       True  -> snd $ unzip l
       False -> error "FetchArrays array length mismatch!"
 
-    go = \case
-      ETuple a -> concatMap go a
-      a -> let A1 "List" (compInputType "compAV" -> t) = tyOf a
-               values = compList a
-           in
-            [(length values,(t,foldr (flatten t) (emptyArray t) values))]
+    go a = (length values,(t,foldr (flatten t) (emptyArray t) values))
+      where (A1 "List" (compInputType "compAV" -> t)) = tyOf a
+            values = map compValue $ compList a
 
 compFetchPrimitive x = case x of
   A0 "Point" -> IR.Points
@@ -512,29 +509,38 @@ genGLSLs backend
         shader $
            uniformDecls fragUniforms
         <> vertOutDecls "in"
-        <> [shaderDecl "out" (toGLSLType "4" tfrag) fragColorName | noUnit tfrag, backend == OpenGL33]
+--        <> [shaderDecl "out" (toGLSLType "4" tfrag) fragColorName | Just{} <- [fragGLSL], backend == OpenGL33]
+        <> [shaderDecl "out" (text t) (text n) | (n, t) <- zip fragOutNames fragOuts, backend == OpenGL33]
         <> fragFuncs
         <> [mainFunc $
                [shaderStmt $ "if" <+> parens ("!" <> parens filt) <+> "discard" | Just filt <- [filtGLSL]]
-            <> [shaderLet fragColorName $ fromMaybe (text $ head vertOutNames) fragGLSL | noUnit tfrag]
+            <> [shaderLet (text n) x | (n, x) <- zip fragOutNames fragGLSL ]
            ]
       )
   where
     uniformDecls us = [shaderDecl "uniform" (text $ showGLSLType "2" t) (text n) | (n, (_, t)) <- Map.toList us]
     vertOutDecls io = [shaderDecl (caseWO "varying" $ text i <+> io) (text t) (text n) | (n, (i, t)) <- zip vertOutNames vertOuts]
 
+    fragOutNames = case length frags of
+        0 -> []
+        1 -> [caseWO (head vertOutNames) fragColorName]
+
     (vertIns, verts) = case vert of
-        Just (etaRed -> Just (vertIns, verts)) -> (toGLSLType "3" <$> vertIns, eTuple verts)
-        Nothing      -> ([], [mkTVar 0 tvert])
+        Just (etaReds -> Just (xs, ys)) -> (toGLSLType "3" <$> xs, eTuple ys)
+        Nothing -> ([toGLSLType "4" tvert], [mkTVar 0 tvert])
+
+    (fragOuts, frags) = case frag of
+        Just (etaReds -> Just (xs, eTuple -> ys)) -> (toGLSLType "3" . tyOf <$> ys, ys)
+        Nothing -> ([toGLSLType "4" tfrag], [mkTVar 0 tfrag])
 
     (((vertGLSL, ptGLSL), (vertUniforms, vertFuncs)), ((filtGLSL, fragGLSL), (fragUniforms, fragFuncs))) = flip evalState shaderNames $ do
         ((g1, (us1, verts)), (g2, (us2, frags))) <- (,)
             <$> runWriterT ((,)
-                <$> traverse (genGLSL' vertInNames . (,) vertIns) verts
-                <*> traverse (genGLSL' vertOutNamesWithPosition . red) rp)
+                <$> traverse (genGLSL' "1" vertInNames . (,) vertIns) verts
+                <*> traverse (genGLSL' "2" vertOutNamesWithPosition . reds) rp)
             <*> runWriterT ((,)
-                <$> traverse (genGLSL' vertOutNames . red) ffilter
-                <*> traverse (genGLSL' vertOutNames . red) frag)
+                <$> traverse (genGLSL' "3" vertOutNames . red) ffilter
+                <*> traverse (genGLSL' "4" vertOutNames . (,) (snd <$> vertOuts)) frags)
         (,) <$> ((,) g1 <$> fixFuncs us1 mempty [] verts) <*> ((,) g2 <$> fixFuncs us2 mempty [] frags)
 
     fixFuncs :: Uniforms -> Set.Set SName -> [Doc] -> Map.Map SName (ExpTV, ExpTV, [ExpTV]) -> State [SName] (Uniforms, [Doc])
@@ -558,11 +564,13 @@ genGLSLs backend
     vertOutNames = map (("vo" ++) . show) [1..length vertOuts]
     vertOutNamesWithPosition = "gl_Position": vertOutNames
 
-    red (etaRed -> Just (ps, o)) = (ps, o)
+    red (etaReds -> Just (ps, o)) = (ps, o)
     red x = error $ "red: " ++ ppShow x
-    genGLSL' vertOuts (ps, o)
+    reds (etaReds -> Just (ps, o)) = (ps, o)
+    reds x = error $ "red: " ++ ppShow x
+    genGLSL' err vertOuts (ps, o)
         | length ps == length vertOuts = genGLSL (reverse vertOuts) o
-        | otherwise = error $ "makeSubst illegal input " ++ show ps ++ "\n" ++ show vertOuts
+        | otherwise = error $ "makeSubst illegal input " ++ err ++ "  " ++ show ps ++ "\n" ++ show vertOuts
 
     noUnit TTuple0 = False
     noUnit _ = True
@@ -596,10 +604,6 @@ genGLSLs backend
 
     caseWO w o = case backend of WebGL1 -> w; OpenGL33 -> o
 
-
-eTuple (ETuple l) = l
-eTuple x = [x]
-
 data Uniform
     = UUniform
     | UTexture2DSlot
@@ -753,7 +757,6 @@ genGLSL dns e = case e of
     -- not supported
     n | n `elem` ["primIntToWord", "primIntToFloat", "primCompareInt", "primCompareWord", "primCompareFloat"] -> error $ "WebGL 1 does not support: " ++ ppShow e
     n | n `elem` ["M23F", "M24F", "M32F", "M34F", "M42F", "M43F"] -> error "WebGL 1 does not support matrices with this dimension"
-    (tupName -> Just n) -> pure $ error "GLSL codegen for tuple is not supported yet"
     x -> error $ "GLSL codegen - unsupported function: " ++ ppShow x
 
   x -> error $ "GLSL codegen - unsupported expression: " ++ ppShow x
@@ -907,18 +910,20 @@ removeLams 0 x = x
 removeLams i (ELam _ x) = removeLams (i-1) x
 removeLams i (Lam Hidden _ x) = removeLams i x
 
-etaRed (ELam _ (App (down 0 -> Just f) (EVar 0))) = etaRed f
-etaRed (ELam _ (A3 (tupCaseName -> Just k) _ (down 0 -> Just x) (EVar 0))) = Just $ getPats k x
-etaRed (ELam p i) = Just (getPVars p, i)
---etaRed x | Pi Visible a b <- tyOf x = Just ([mkTVar 0 a], App x $ mkTVar 0 a)
-etaRed x = Nothing
+etaReds (ELam _ (App (down 0 -> Just f) (EVar 0))) = etaReds f
+etaReds (ELam _ (hlistLam -> x@Just{})) = x
+etaReds (ELam p i) = Just ([p], i)
+etaReds x = Nothing
 
-getPVars = \case
-    TTuple0 -> []
-    t -> [t]
+hlistLam :: ExpTV -> Maybe ([ExpTV], ExpTV)
+hlistLam (A3 "hlistNilCase" _ (down 0 -> Just x) (EVar 0)) = Just ([], x)
+hlistLam (A3 "hlistConsCase" _ (down 0 -> Just (getPats 2 -> Just ([p, px], x))) (EVar 0)) = first (p:) <$> hlistLam x
+hlistLam _ = Nothing
 
-getPats 0 e = ([], e)
-getPats i (ELam p e) = first (p:) $ getPats (i-1) e
+getPats 0 e = Just ([], e)
+getPats i (ELam p e) = first (p:) <$> getPats (i-1) e
+getPats i (Lam Hidden p (down 0 -> Just e)) = getPats i e
+getPats i x = error $ "getPats: " ++ show i ++ " " ++ ppShow x
 
 pattern EtaPrim1 s <- (getEtaPrim -> Just (s, []))
 pattern EtaPrim2 s x <- (getEtaPrim -> Just (s, [x]))
@@ -936,14 +941,6 @@ getEtaPrim2 _ = Nothing
 initLast [] = Nothing
 initLast xs = Just (init xs, last xs)
 
-tupCaseName "Tuple2Case" = Just 2
-tupCaseName "Tuple3Case" = Just 3
-tupCaseName "Tuple4Case" = Just 4
-tupCaseName "Tuple5Case" = Just 5
-tupCaseName "Tuple6Case" = Just 6
-tupCaseName "Tuple7Case" = Just 7
-tupCaseName _ = Nothing
-
 -------------
 
 pattern EVar n <- Var n _
@@ -956,7 +953,7 @@ pattern A3 n a b c <- Con n [a, b, c]
 pattern A4 n a b c d <- Con n [a, b, c, d]
 pattern A5 n a b c d e <- Con n [a, b, c, d, e]
 
-pattern TTuple0     <- A0 "Tuple0"
+pattern TTuple0     <- A1 "HList" (A0 "Nil")
 pattern TBool       <- A0 "Bool"
 pattern TWord       <- A0 "Word"
 pattern TInt        <- A0 "Int"
@@ -976,16 +973,12 @@ fromNat _ = Nothing
 pattern TTuple xs <- ETuple xs
 pattern ETuple xs <- (getTuple -> Just xs)
 
-getTuple (Con (tupName -> Just n) xs) | length xs == n = Just xs
-getTuple _ = Nothing
+eTuple (ETuple l) = l
+eTuple x | A1 "HList" _ <- tyOf x = error $ "eTuple: " ++ ppShow x --[x]
+eTuple x = [x]
 
-tupName = \case
-    "Tuple0" -> Just 0
-    "Tuple2" -> Just 2
-    "Tuple3" -> Just 3
-    "Tuple4" -> Just 4
-    "Tuple5" -> Just 5
-    "Tuple6" -> Just 6
-    "Tuple7" -> Just 7
-    _ -> Nothing
+getTuple (A1 "HList" l) = Just $ compList l
+getTuple (A0 "HNil") = Just []
+getTuple (A2 "HCons" x (getTuple -> Just xs)) = Just (x: xs)
+getTuple _ = Nothing
 
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 79a97a09..9afa8a36 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -28,7 +28,6 @@ module LambdaCube.Compiler.Infer
     , nType, conType, neutType, neutType', appTy, mkConPars, makeCaseFunPars, makeCaseFunPars'
     , MaxDB(..), unfixlabel
     , ErrorMsg, showError
-    , extractDesugarInfo
     ) where
 
 import Data.Monoid
@@ -165,20 +164,12 @@ pattern TFloat      <- TTyCon0 "'Float"     where TFloat = tTyCon0 "'Float" $ er
 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 TInterpolated a <- TyConN "'Interpolated" [a] 
-tFloating t = error "tFloating" --TFun "'Floating" (TType :~> TType) [t]
-tInterpolated x = tTyCon "'Interpolated" (TType :~> TType) [x] [Pi Hidden TType $ Pi Hidden (tFloating $ Var 0) $ tInterpolated $ Var 1, error "cs 12'", error "cs 12''"]
-pattern TList a     <- TyConN "'List" [a] where TList a = tTyCon "'List" (TType :~> TType) [a] $ error "cs 11"
+
 pattern Empty s   <- TyCon (TyConName "'Empty" _ _ _ _) [EString s] where
         Empty s    = TyCon (TyConName "'Empty" (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [EString s]
 
 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 [])
 pattern Succ n      <- ConN "Succ" (n:_) where Succ n = tCon "Succ" 1 (TNat :~> TNat) [n]
 
@@ -197,8 +188,6 @@ 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)
-
 toNatE :: Int -> Exp
 toNatE 0         = Zero
 toNatE n | n > 0 = Closed (Succ (toNatE (n - 1)))
@@ -225,13 +214,10 @@ mkOrdering x = Closed $ case x of
     EQ -> tCon "EQ" 1 TOrdering []
     GT -> tCon "GT" 2 TOrdering []
 
-noTup (TyConN s _) = take 6 s /= "'Tuple" -- todo
-noTup _ = False
-
 conTypeName :: ConName -> TyConName
 conTypeName (ConName _ _ t) = case snd $ getParams t of TyCon n _ -> n
 
-outputType = TOutput
+outputType = tTyCon0 "'Output" $ error "cs 9"
 boolType = TBool
 trueExp = EBool True
 
@@ -478,6 +464,9 @@ getFunDef s f = case s of
         parEval _ _ (LabelEnd x) = LabelEnd x
         parEval t a b = ParEval t a b
 
+    "hlistNilCase" -> \case [_, x, unfixlabel -> Con n@(ConName _ 0 _) _ []] -> x; xs -> f xs
+    "hlistConsCase" -> \case [_, _, _, x, unfixlabel -> Con n@(ConName _ 1 _) _ [_, _, a, b]] -> x `app_` a `app_` b; xs -> f xs
+
     -- general compiler primitives
     "primAddInt" -> \case [EInt i, EInt j] -> EInt (i + j); xs -> f xs
     "primSubInt" -> \case [EInt i, EInt j] -> EInt (i - j); xs -> f xs
@@ -520,40 +509,27 @@ getFunDef s f = case s of
 
 cstr = f []
   where
-    f _ _ a a' | unfixlabel a == unfixlabel a' = Unit
-    f ns typ (LabelEnd a) (LabelEnd a') = f ns typ a a'
-    f ns typ (FL a) a' = f ns typ a a'
-    f ns typ a (FL 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 (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'
-    f ns TType (Pi h a b) (Pi h' a' b') | h == h' = t2 (f ns TType a a') (f ((a, a'): ns) TType b b')
-
-    f [] TType (UFunN "'VecScalar" [a, b]) (TVec a' b') = t2 (f [] TNat a a') (f [] TType b b')
-    f [] TType (UFunN "'VecScalar" [a, b]) (UFunN "'VecScalar" [a', b']) = t2 (f [] TNat a a') (f [] TType b b')
-    f [] TType (UFunN "'VecScalar" [a, b]) t@(TTyCon0 n) | isElemTy n = t2 (f [] TNat a (ENat 1)) (f [] TType b t)
-    f [] TType t@(TTyCon0 n) (UFunN "'VecScalar" [a, b]) | isElemTy n = t2 (f [] TNat a (ENat 1)) (f [] TType b t)
-
---    f [] TType (UTFun "map" (Pi _ t _) [a, b]) (TyConN ":" [x, xs]) = f [] t a (cons x nil)
+    f z ty a a' = f_ z (unfixlabel ty) (unfixlabel a) (unfixlabel a')
 
-    f [] TType (UTFun "'FragOps" (Pi _ t _) [a]) (TyConN "'FragmentOperation" [x]) = f [] t a (cons x nil)
-    f [] TType (UTFun "'FragOps" (Pi _ t _) [a]) (TyConN "'Tuple2" [TyConN "'FragmentOperation" [x], TyConN "'FragmentOperation" [y]]) = f [] t a $ cons x $ cons y nil
-
-    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' TTuple0)
+    f_ _ _ a a' | a == a' = Unit
+    f_ ns typ (LabelEnd a) (LabelEnd 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' = 
+        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'
+    f_ ns TType (Pi h a b) (Pi h' a' b') | h == h' = t2 (f ns TType a a') (f ((a, a'): ns) TType b b')
 
---    f ns@[] TType (UFunN "'InterpolatedType" [x'@Neut{}]) TTuple0 = f ns TType x' TTuple0
---    f ns@[] TType (UFunN "'InterpolatedType" [x'@Neut{}]) x@NoTup = f ns TType (tInterpolated x') x
---    f ns@[] TType (UFunN "'InterpolatedType" [x'@Neut{}]) (TInterpolated x) = f ns TType x' x
-    f ns@[] TType x@NoTup (UFunN "'InterpolatedType" [x'@Neut{}]) = f ns TType (tInterpolated x) x'
+    f_ [] TType (UFunN "'VecScalar" [a, b]) (UFunN "'VecScalar" [a', b']) = t2 (f [] TNat a a') (f [] TType b b')
+    f_ [] TType (UFunN "'VecScalar" [a, b]) (TVec a' b') = t2 (f [] TNat a a') (f [] TType b b')
+    f_ [] TType (UFunN "'VecScalar" [a, b]) t@(TTyCon0 n) | isElemTy n = t2 (f [] TNat a (ENat 1)) (f [] TType b t)
+    f_ [] TType (TVec a' b') (UFunN "'VecScalar" [a, b]) = t2 (f [] TNat a' a) (f [] TType b' b)
+    f_ [] TType t@(TTyCon0 n) (UFunN "'VecScalar" [a, b]) | isElemTy n = t2 (f [] TNat a (ENat 1)) (f [] TType b t)
 
-    f [] typ a@Neut{} a' = CstrT typ a a'
-    f [] typ a a'@Neut{} = CstrT typ a a'
+    f_ [] typ a@Neut{} a' = CstrT typ a a'
+    f_ [] typ a a'@Neut{} = CstrT typ a a'
 
-    f ns typ a a' = Empty $ unlines [ "can not unify"
+    f_ ns typ a a' = Empty $ unlines [ "can not unify"
                                     , ppShow a
                                     , "with"
                                     , ppShow a'
@@ -688,15 +664,7 @@ parent = \case
     CheckAppType _ _ _ x _ -> Right x
     ELabelEnd x          -> Right x
     EGlobal              -> Left ()
-{-
-freeVars = \case
-    EGlobal -> []
-    EAssign i _ x -> [Var $ if j > i then j-1 else j | Var j <- freeVars x, j /= i]
-    EBind2 _ _ x -> Var 0: (up 1 <$> freeVars x)
-    ELet2 _ _ x -> Var 0: (up 1 <$> freeVars x)
-    x | Right y <- parent x -> freeVars y
-    x -> error $ "freeVars: " ++ show x
--}
+
 -------------------------------------------------------------------------------- simple typing
 
 litType = \case
@@ -769,17 +737,10 @@ expAndType s (e, t, si) = (e, t)
 -- todo: do only if NoTypeNamespace extension is not on
 lookupName s@('\'':s') m = expAndType s <$> (Map.lookup s m `mplus` Map.lookup s' m)
 lookupName s m           = expAndType s <$> Map.lookup s m
---elemIndex' s@('\'':s') m = elemIndex s m `mplus` elemIndex s' m
---elemIndex' s m = elemIndex s m
 
 getDef te si s = do
     nv <- asks snd
     maybe (throwError' $ ECantFind s si) return (lookupName s nv)
-{-
-take' e n xs = case splitAt n xs of
-    (as, []) -> as
-    (as, _) -> as ++ [e]
--}
 
 type ExpType' = CEnv ExpType
 
@@ -799,6 +760,7 @@ inferN_ tellTrace = infer  where
 
     infer :: Env -> SExp2 -> IM m ExpType'
     infer te exp = tellTrace "infer" (showEnvSExp te exp) $ (if debug then fmap (fmap{-todo-} $ recheck' "infer" te) else id) $ case exp of
+        Parens x        -> infer te x
         SAnn x t        -> checkN (CheckIType x te) t TType
         SLabelEnd x     -> infer (ELabelEnd te) x
         SVar (si, _) i  -> focus_' te exp (Var i, snd $ varType "C2" i te)
@@ -812,6 +774,7 @@ inferN_ tellTrace = infer  where
     checkN :: Env -> SExp2 -> Type -> IM m ExpType'
     checkN te x t = tellTrace "check" (showEnvSExpType te x t) $ checkN_ te x t
 
+    checkN_ te (Parens e) t = checkN_ te e t
     checkN_ te e t
         | x@(SGlobal (si, MatchName n)) `SAppV` SLamV (Wildcard _) `SAppV` a `SAppV` SVar siv v `SAppV` b <- e
             = infer te $ x `SAppV` SLam Visible SType (STyped mempty (subst (v+1) (Var 0) $ up 1 t, TType)) `SAppV` a `SAppV` SVar siv v `SAppV` b
@@ -901,8 +864,10 @@ inferN_ tellTrace = infer  where
 
     focus2 :: Env -> CEnv ExpType -> IM m ExpType'
     focus2 env eet = case env of
+--        ELabelEnd te ->
         ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-}
         EBind2_ si BMeta tt_ te
+            | ELabelEnd te'   <- te -> refocus (ELabelEnd $ EBind2_ si BMeta tt_ te') eet
             | Unit <- tt    -> refocus te $ subst 0 TT eet
             | Empty msg <- tt -> throwError' $ ETypeError msg si
             | T2 x y <- tt, let te' = EBind2_ si BMeta (up 1 y) $ EBind2_ si BMeta x te
@@ -923,7 +888,6 @@ inferN_ tellTrace = infer  where
             | EApp2 si h x te' <- te -> refocus (EApp2 si h (up 1 x) $ EBind2_ si BMeta tt_ te') eet
             | CheckType_ si t te' <- te -> refocus (CheckType_ si (up 1 t) $ EBind2_ si BMeta tt_ te') eet
 --            | CheckIType x te' <- te -> refocus (CheckType_ si (up 1 t) $ EBind2_ si BMeta tt te') eet
-            | ELabelEnd te'   <- te -> refocus (ELabelEnd $ EBind2_ si BMeta tt_ te') eet
             | otherwise             -> focus2 te $ Meta tt_ eet
           where
             tt = unfixlabel tt_
@@ -936,6 +900,7 @@ inferN_ tellTrace = infer  where
                 _ -> Nothing
 
         EAssign i b te -> case te of
+            ELabelEnd te'     -> refocus' (ELabelEnd $ EAssign i b te') eet
             EBind2_ si h x te' | i > 0, Just b' <- down 0 b
                               -> refocus' (EBind2_ si h (subst (i-1) (fst b') x) (EAssign (i-1) b' te')) eet
             ELet2 le (x, xt) te' | i > 0, Just b' <- down 0 b
@@ -946,18 +911,26 @@ inferN_ tellTrace = infer  where
             EApp1 si h te' x  -> refocus' (EApp1 si h (EAssign i b te') $ substS i b x) eet
             EApp2 si h x te'  -> refocus' (EApp2 si h (subst i (fst b) x) $ EAssign i b te') eet
             CheckType_ si t te'   -> refocus' (CheckType_ si (subst i (fst b) t) $ EAssign i b te') eet
-            ELabelEnd te'     -> refocus' (ELabelEnd $ EAssign i b te') eet
             EAssign j a te' | i < j
                               -> refocus' (EAssign (j-1) (subst i (fst b) a) $ EAssign i (up1_ (j-1) b) te') eet
-            t  | Just te' <- pull i te -> refocus' te' eet
-               | otherwise      -> swapAssign (\i x -> focus2 te . Assign i x) (\i x -> refocus' $ EAssign i x te) i b eet
+            t  | Just te' <- pull1 i b te -> refocus' te' eet
+               | otherwise -> swapAssign (\i x -> focus2 te . Assign i x) (\i x -> refocus' $ EAssign i x te) i b eet
             -- todo: CheckSame Exp Env
           where
             refocus' = fix refocus_
+
+            pull1 i b = \case
+                EBind2_ si h x te | i > 0, Just b' <- down 0 b
+                    -> EBind2_ si h (subst (i-1) (fst b') x) <$> pull1 (i-1) b' te
+                EAssign j a te
+                    | i < j  -> EAssign (j-1) (subst i (fst b) a) <$> pull1 i (up1_ (j-1) b) te
+                    | j <= i -> EAssign j (subst i (fst b) a) <$> pull1 (i+1) (up1_ j b) te
+                te  -> pull i te
+
             pull i = \case
                 EBind2 BMeta _ te | i == 0 -> Just te
-                EBind2_ si h x te   -> EBind2_ si h <$> down (i-1) x <*> pull (i-1) te
-                EAssign j b te  -> EAssign (if j <= i then j else j-1) <$> down i b <*> pull (if j <= i then i+1 else i) te
+                EBind2_ si h x te | i > 0 -> EBind2_ si h <$> down (i-1) x <*> pull (i-1) te
+                EAssign j a te  -> EAssign (if j <= i then j else j-1) <$> down i a <*> pull (if j <= i then i+1 else i) te
                 _               -> Nothing
 
         EGlobal{} -> return eet
@@ -1089,30 +1062,13 @@ dependentVars ie = cycle mempty
 
 -------------------------------------------------------------------------------- global env
 
-type GlobalEnv = Map.Map SName (Exp, Type, (SI, MFixity))
+type GlobalEnv = Map.Map SName (Exp, Type, SI)
 
 initEnv :: GlobalEnv
 initEnv = Map.fromList
-    [ (,) "'Type" (TType, TType, (debugSI "source-of-Type", Nothing))
+    [ (,) "'Type" (TType, TType, debugSI "source-of-Type")
     ]
 
--- todo: eliminate
-extractDesugarInfo :: GlobalEnv -> DesugarInfo
-extractDesugarInfo ge =
-    ( Map.fromList
-        [ (n, f) | (n, (d, _, (si, Just f))) <- Map.toList ge ]
-    , Map.fromList $
-        [ (n, Left ((t, inum), map f cons))
-        | (n, ( (Con cn 0 []), _, si)) <- Map.toList ge, let TyConName t inum _ cons _ = conTypeName cn
-        ] ++
-        [ (n, Right $ pars t)
-        | (n, ( (TyCon (TyConName _ _ t _ _) []), _, _)) <- Map.toList ge
-        ]
-    )
-  where
-    f (ConName n _ _, ct) = (n, pars ct)
-    pars = length . filter ((==Visible) . fst) . fst . getParams
-
 -------------------------------------------------------------------------------- infos
 
 data Info
@@ -1156,16 +1112,16 @@ listTypeInfos m = map (second Set.toList) $ Map.toList $ Map.unionsWith (<>) [Ma
 
 handleStmt :: MonadFix m => [Stmt] -> Stmt -> IM m GlobalEnv
 handleStmt defs = \case
-  Primitive n mf (trSExp' -> t_) -> do
+  Primitive n (trSExp' -> t_) -> do
         t <- inferType =<< ($ t_) <$> addF
         tellType (fst n) t
-        addToEnv n mf $ flip (,) t $ lamify t $ Neut . DFun_ (FunName (snd n) Nothing t)
-  Let n mf mt t_ -> do
+        addToEnv n $ flip (,) t $ lamify t $ Neut . DFun_ (FunName (snd n) Nothing t)
+  Let n mt t_ -> do
         af <- addF
         let t__ = maybe id (flip SAnn . af) mt t_
         (x, t) <- inferTerm (snd n) $ trSExp' $ if usedS n t__ then SBuiltin "primFix" `SAppV` SLamV (substSG0 n t__) else t__
         tellType (fst n) t
-        addToEnv n mf (mkELet n x t, t)
+        addToEnv n (mkELet n x t, t)
 {-        -- hack
         when (snd (getParams t) == TType) $ do
             let ps' = fst $ getParams t
@@ -1194,7 +1150,7 @@ handleStmt defs = \case
                         act = length . fst . getParams $ cty
                         acts = map fst . fst . getParams $ cty
                         conn = ConName (snd cn) j cty
-                e <- addToEnv cn (listToMaybe [f | PrecDef n f <- defs, n == cn]) (Con conn 0 [], cty)
+                e <- addToEnv cn (Con conn 0 [], cty)
                 return (e, ((conn, cty)
                        , addParamsS pars
                        $ foldl SAppV (SVar (debugSI "22", ".cs") $ j + length pars) $ drop pnum' xs ++ [apps' (SGlobal cn) (zip acts $ downToS ("a4 " ++ snd cn ++ " " ++ show (length ps)) (j+1+length pars) (length ps) ++ downToS "a5" 0 (act- length ps))]
@@ -1209,7 +1165,7 @@ handleStmt defs = \case
     (e1, es, tcn, cfn@(CaseFunName _ ct _), _, _) <- mfix $ \ ~(_, _, _, _, ct', cons') -> do
         let cfn = CaseFunName (snd s) ct' $ length ps
         let tcn = TyConName (snd s) inum vty (map fst cons') cfn
-        e1 <- addToEnv s (listToMaybe [f | PrecDef n f <- defs, n == s]) (TyCon tcn [], vty)
+        e1 <- addToEnv s (TyCon tcn [], vty)
         (unzip -> (mconcat -> es, cons)) <- withEnv e1 $ zipWithM mkConstr [0..] cs
         ct <- withEnv (e1 <> es) $ inferType
             ( (\x -> traceD ("type of case-elim before elaboration: " ++ ppShow x) x) $ addParamsS
@@ -1223,14 +1179,14 @@ handleStmt defs = \case
             )
         return (e1, es, tcn, cfn, ct, cons)
 
-    e2 <- addToEnv (fst s, caseName (snd s)) Nothing (lamify ct $ \xs -> evalCaseFun cfn (init $ drop (length ps) xs) (last xs), ct)
+    e2 <- addToEnv (fst s, caseName (snd s)) (lamify ct $ \xs -> evalCaseFun cfn (init $ drop (length ps) xs) (last xs), ct)
     let ps' = fst $ getParams vty
         t =   (TType :~> TType)
           :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo 0 $ length ps'))
           :~>  TType
           :~> Var 2 `app_` Var 0
           :~> Var 3 `app_` Var 1
-    e3 <- addToEnv (fst s, MatchName (snd s)) Nothing (lamify t $ \[m, tr, n, f] -> evalTyCaseFun (TyCaseFunName (snd s) t) [m, tr, f] n, t)
+    e3 <- addToEnv (fst s, MatchName (snd s)) (lamify t $ \[m, tr, n, f] -> evalTyCaseFun (TyCaseFunName (snd s) t) [m, tr, f] n, t)
     return (e1 <> e2 <> e3 <> es)
 
   stmt -> error $ "handleStmt: " ++ show stmt
@@ -1280,15 +1236,15 @@ inferTerm msg t =
 inferType :: Monad m => SExp2 -> IM m Type
 inferType t = fmap (closedExp . fst . recheck "inferType" EGlobal . flip (,) TType . replaceMetas (Pi Hidden) . fmap fst) $ inferN (CheckType_ (debugSI "inferType CheckType_") TType EGlobal) t
 
-addToEnv :: Monad m => SIName -> MFixity -> ExpType -> IM m GlobalEnv
-addToEnv (si, s) mf (x, t) = do
+addToEnv :: Monad m => SIName -> ExpType -> IM m GlobalEnv
+addToEnv (si, s) (x, t) = do
 --    maybe (pure ()) throwError_ $ ambiguityCheck s t      -- TODO
 --    b <- asks $ (TraceTypeCheck `elem`) . fst
     tell [IType s $ ppShow t]
     v <- asks $ Map.lookup s . snd
     case v of
-      Nothing -> return $ Map.singleton s (closedExp x, closedExp t, (si, mf))
-      Just (_, _, (si', _)) -> throwError' $ ERedefined s si si'
+      Nothing -> return $ Map.singleton s (closedExp x, closedExp t, si)
+      Just (_, _, si') -> throwError' $ ERedefined s si si'
 {-
 joinEnv :: Monad m => GlobalEnv -> GlobalEnv -> IM m GlobalEnv
 joinEnv e1 e2 = do
@@ -1308,6 +1264,7 @@ tellType si t = tell $ mkInfoItem (sourceInfo si) $ removeEscs $ showDoc $ mkDoc
 data PolyEnv = PolyEnv
     { getPolyEnv :: GlobalEnv
     , infos      :: Infos
+    , dsInfo     :: DesugarInfo
     }
 
 filterPolyEnv p pe = pe { getPolyEnv = Map.filterWithKey (\k _ -> p k) $ getPolyEnv pe }
@@ -1315,8 +1272,8 @@ filterPolyEnv p pe = pe { getPolyEnv = Map.filterWithKey (\k _ -> p k) $ getPoly
 joinPolyEnvs :: MonadError String m => Bool -> [PolyEnv] -> m PolyEnv
 joinPolyEnvs _ = return . foldr mappend' mempty'           -- todo
   where
-    mempty' = PolyEnv mempty mempty
-    PolyEnv a b `mappend'` PolyEnv a' b' = PolyEnv (a `mappend` a') (b `mappend` b')
+    mempty' = PolyEnv mempty mempty mempty
+    PolyEnv a b c `mappend'` PolyEnv a' b' c' = PolyEnv (a `mappend` a') (b `mappend` b') (c `joinDesugarInfo` c')
 
 -------------------------------------------------------------------------------- pretty print
 -- todo: do this via conversion to SExp
@@ -1403,9 +1360,11 @@ instance MkDoc Exp where
       where
         f = \case
 --            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)
+            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
+            (getTTup -> Just xs) -> shTuple <$> mapM f xs
+            (getTup -> Just xs) -> shTuple <$> mapM f xs
             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"
@@ -1440,19 +1399,31 @@ instance MkDoc (CEnv Exp) where
             Meta a b        -> join $ shLam True BMeta <$> mkDoc ts a <*> pure (f b)
             Assign i (x, _) e -> shLet i (mkDoc ts x) (f e)
 
+getTup (unfixlabel -> ConN "HCons" [_, _, x, xs]) = (x:) <$> getTup xs
+getTup (unfixlabel -> ConN "HNil" []) = Just []
+getTup _ = Nothing
+
+getTTup (unfixlabel -> TyConN "'HList" [xs]) = getList xs
+getTTup _ = Nothing
+
+getList (unfixlabel -> ConN "Cons" [x, xs]) = (x:) <$> getList xs
+getList (unfixlabel -> ConN "Nil" []) = Just []
+getList _ = Nothing
+
+
 -------------------------------------------------------------------------------- main
 
 mfix' f = ExceptT (mfix (runExceptT . f . either bomb id))
   where bomb e = error $ "mfix (ExceptT): inner computation returned Left value:\n" ++ show e
 
 inference_ :: PolyEnv -> Extensions -> [Stmt] -> ExceptT ErrorMsg (WriterT Infos Identity) PolyEnv
-inference_ (PolyEnv pe is) exts defs = mapExceptT (ff . runWriter . flip runReaderT (exts, mempty)) $ gg (handleStmt defs) (initEnv <> pe) defs
+inference_ (PolyEnv pe is _) exts defs = mapExceptT (ff . runWriter . flip runReaderT (exts, mempty)) $ gg (handleStmt defs) (initEnv <> pe) defs
   where
     ff (Left e, is) = do
         tell is
         return $ Left e
     ff (Right ge, is) = do
-        return $ Right $ PolyEnv ge is
+        return $ Right $ PolyEnv ge is $ mkDesugarInfo defs
 
     gg _ acc [] = return acc
     gg m acc (x:xs) = do
diff --git a/src/LambdaCube/Compiler/Lexer.hs b/src/LambdaCube/Compiler/Lexer.hs
index 1389ebf2..631bbef9 100644
--- a/src/LambdaCube/Compiler/Lexer.hs
+++ b/src/LambdaCube/Compiler/Lexer.hs
@@ -52,7 +52,7 @@ type PostponedCheck = Maybe String
 type DesugarInfo = (FixityMap, ConsMap)
 
 type ConsMap = Map.Map SName{-constructor name-}
-                (Either ((SName{-type name-}, Int{-num of indices-}), [(SName, Int)]{-constructors with arities-})
+                (Either ((SName{-case eliminator name-}, Int{-num of indices-}), [(SName, Int)]{-constructors with arities-})
                         Int{-arity-})
 
 dsInfo :: P DesugarInfo
@@ -253,7 +253,6 @@ upperLower      = lowerCase <|> upperCase_ <|> parens (symbols <|> backquotedIde
 
 data FixityDef = Infix | InfixL | InfixR deriving (Show)
 type Fixity = (FixityDef, Int)
-type MFixity = Maybe Fixity
 type FixityMap = Map.Map SName Fixity
 
 calcPrec
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 6a27fb56..e4d482a8 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -13,14 +13,14 @@ module LambdaCube.Compiler.Parser
     , sourceInfo, SI(..), debugSI
     , Module(..), Visibility(..), Binder(..), SExp'(..), Extension(..), Extensions
     , pattern SVar, pattern SType, pattern Wildcard, pattern SAppV, pattern SLamV, pattern SAnn
-    , pattern SBuiltin, pattern SPi, pattern Primitive, pattern SLabelEnd, pattern SLam
+    , pattern SBuiltin, pattern SPi, pattern Primitive, pattern SLabelEnd, pattern SLam, pattern Parens
     , pattern TyType, pattern Wildcard_
     , debug, isPi, varDB, lowerDB, justDB, upDB, cmpDB, MaxDB (..), iterateN, traceD
     , parseLC, runDefParser
     , getParamsS, addParamsS, getApps, apps', downToS, addForalls
     , mkDesugarInfo, joinDesugarInfo
     , Up (..), up1, up
-    , Doc, shLam, shApp, shLet, shLet_, shAtom, shAnn, shVar, epar, showDoc, showDoc_, sExpDoc, shCstr
+    , Doc, shLam, shApp, shLet, shLet_, shAtom, shAnn, shVar, epar, showDoc, showDoc_, sExpDoc, shCstr, shTuple
     , mtrace, sortDefs
     , trSExp', usedS, substSG0, substS
     , Stmt (..), Export (..), ImportItems (..)
@@ -131,6 +131,7 @@ pattern SLabelEnd a = SBuiltin "labelend" `SAppV` a
 pattern SBuiltin s <- SGlobal (_, s) where SBuiltin s = SGlobal (debugSI $ "builtin " ++ s, s)
 
 pattern Section e = SBuiltin "^section"  `SAppV` e
+pattern Parens e = SBuiltin "parens"  `SAppV` e
 
 sApp v a b = SApp (sourceInfo a <> sourceInfo b) v a b
 sBind v x a b = SBind (sourceInfo a <> sourceInfo b) v x a b
@@ -398,25 +399,24 @@ parseTerm prec = setSI' {-TODO: remove, slow-} $ case prec of
 
     mkProjection = foldl $ \exp field -> SBuiltin "project" `SAppV` field `SAppV` exp
 
-    -- Creates: RecordCons @[("x", _), ("y", _), ("z", _)] (1.0, (2.0, (3.0, ())))
+    -- Creates: RecordCons @[("x", _), ("y", _), ("z", _)] (1.0, 2.0, 3.0)))
     mkRecord xs = SBuiltin "RecordCons" `SAppH` names `SAppV` values
       where
         (names, values) = mkNames *** mkValues $ unzip xs
 
-        mkNameTuple (si, v) = SBuiltin "Tuple2" `SAppV` SLit si (LString v) `SAppV` Wildcard SType
+        mkNameTuple (si, v) = SBuiltin "RecItem" `SAppV` SLit si (LString v) `SAppV` Wildcard SType
         mkNames = foldr (\n ns -> SBuiltin "Cons" `SAppV` mkNameTuple n `SAppV` ns)
                         (SBuiltin "Nil")
 
-        mkValues = foldr (\x xs -> SBuiltin "Tuple2" `SAppV` x `SAppV` xs)
-                         (SBuiltin "Tuple0")
+        mkValues = foldr (\x xs -> SBuiltin "HCons" `SAppV` x `SAppV` xs)
+                         (SBuiltin "HNil")
 
     mkTuple _ [Section e] = e
-    mkTuple _ [x] = x
-    mkTuple (Namespace level _) xs = foldl SAppV (SBuiltin (tuple ++ show (length xs))) xs
-      where tuple = case level of
-                Just TypeLevel -> "'Tuple"
-                Just ExpLevel -> "Tuple"
-                _ -> error "mkTuple"
+    mkTuple (Namespace (Just TypeLevel) _) [Parens e] = SBuiltin "'HList" `SAppV` (SBuiltin "Cons" `SAppV` e `SAppV` SBuiltin "Nil")
+    mkTuple _ [Parens e] = SBuiltin "HCons" `SAppV` e `SAppV` SBuiltin "HNil"
+    mkTuple _ [x] = Parens x
+    mkTuple (Namespace (Just TypeLevel) _) xs = SBuiltin "'HList" `SAppV` foldr (\x y -> SBuiltin "Cons" `SAppV` x `SAppV` y) (SBuiltin "Nil") xs
+    mkTuple _ xs = foldr (\x y -> SBuiltin "HCons" `SAppV` x `SAppV` y) (SBuiltin "HNil") xs
 
     mkList (Namespace (Just TypeLevel) _) [x] = SBuiltin "'List" `SAppV` x
     mkList (Namespace (Just ExpLevel)  _) xs = foldr (\x l -> SBuiltin "Cons" `SAppV` x `SAppV` l) (SBuiltin "Nil") xs
@@ -469,11 +469,11 @@ parseTerm prec = setSI' {-TODO: remove, slow-} $ case prec of
 
     sNonDepPi h a b = SPi h a $ up1 b
 
-getTTuple' (getTTuple -> Just (n, xs)) | n == length xs = xs
+getTTuple' (SBuiltin "'HList" `SAppV` (getTTuple -> Just (n, xs))) | n == length xs = xs
 getTTuple' x = [x]
 
-getTTuple (SAppV (getTTuple -> Just (n, xs)) z) = Just (n, xs ++ [z]{-todo: eff-})
-getTTuple (SGlobal (si, s@(splitAt 6 -> ("'Tuple", reads -> [(n, "")])))) = Just (n :: Int, [])
+getTTuple (SBuiltin "Nil") = Just (0, [])
+getTTuple (SBuiltin "Cons" `SAppV` x `SAppV` (getTTuple -> Just (n, y))) = Just (n+1, x:y)
 getTTuple _ = Nothing
 
 patLam :: (SExp -> SExp) -> DesugarInfo -> (Visibility, SExp) -> Pat -> SExp -> SExp
@@ -488,6 +488,8 @@ data Pat
     | PatType ParPat SExp
   deriving Show
 
+pattern PParens p = ViewPat (SBuiltin "parens") (ParPat [p])
+
 -- parallel patterns like  v@(f -> [])@(Just x)
 newtype ParPat = ParPat [Pat]
   deriving Show
@@ -499,6 +501,7 @@ mapP :: (SExp -> SExp) -> Pat -> Pat
 mapP f = \case
     PVar n -> PVar n
     PCon n pp -> PCon n (mapPP f <$> pp)
+    PParens p -> PParens (mapP f p)
     ViewPat e pp -> ViewPat (f e) (mapPP f pp)
     PatType pp e -> PatType (mapPP f pp) (f e)
 
@@ -517,6 +520,7 @@ getPPVars = reverse . getPPVars_
 getPVars_ = \case
     PVar n -> [n]
     PCon _ pp -> foldMap getPPVars_ pp
+    PParens p -> getPVars_ p
     ViewPat e pp -> getPPVars_ pp
     PatType pp e -> getPPVars_ pp
 
@@ -577,8 +581,11 @@ parsePat = \case
     mkListPat _ [] = PCon (debugSI "mkListPat3", "Nil") []
 
     --mkTupPat :: [Pat] -> Pat
-    mkTupPat ns [x] = x
-    mkTupPat ns ps = PCon (debugSI "", tick ns $ "Tuple" ++ show (length ps)) (ParPat . (:[]) <$> ps)
+    mkTupPat ns [PParens x] = ff [x]
+    mkTupPat ns [x] = PParens x
+    mkTupPat ns ps = ff ps
+
+    ff ps = foldr (\a b -> PCon (mempty, "HCons") (ParPat . (:[]) <$> [a, b])) (PCon (mempty, "HNil") []) ps
 
     patType p (Wildcard SType) = p
     patType p t = PatType (ParPat [p]) t
@@ -590,6 +597,7 @@ longPattern = parsePat PrecAnn <&> (getPVars &&& id)
 
 telescopePat = fmap (getPPVars . ParPat . map snd &&& id) $ many $ uncurry f <$> hiddenTerm (parsePat PrecAtom) (parsePat PrecAtom)
   where
+    f h (PParens p) = second PParens $ f h p
     f h (PatType (ParPat [p]) t) = ((h, t), p)
     f h p = ((h, Wildcard SType), p)
 
@@ -636,8 +644,10 @@ compilePatts ps gu = cp [] ps
             ]
     cp ps' ((p@PVar{}, i): xs) = cp (p: ps') xs
     cp ps' ((p@(PCon (si, n) ps), i): xs) = GuardNode (SVar (si, n) $ i + sum (map (fromMaybe 0 . ff) ps')) n ps $ cp (p: ps') xs
+    cp ps' ((PParens p, i): xs) = cp ps' ((p, i): xs)
     cp ps' ((p@(ViewPat f (ParPat [PCon (si, n) ps])), i): xs)
         = GuardNode (SAppV f $ SVar (si, n) $ i + sum (map (fromMaybe 0 . ff) ps')) n ps $ cp (p: ps') xs
+    cp _ p = error $ "cp: " ++ show p
 
     m = length ps
 
@@ -670,8 +680,8 @@ compileGuardTree ulend lend adts t = (\x -> traceD ("  !  :" ++ ppShow x) x) $ g
         GuardLeaf e: _ -> lend e
         ts@(GuardNode f s _ _: _) -> case Map.lookup s (snd adts) of
             Nothing -> error $ "Constructor is not defined: " ++ s
-            Just (Left ((t, inum), cns)) ->
-                foldl SAppV (SGlobal (debugSI "compileGuardTree2", caseName t) `SAppV` iterateN (1 + inum) SLamV (Wildcard SType))
+            Just (Left ((casename, inum), cns)) ->
+                foldl SAppV (SGlobal (debugSI "compileGuardTree2", casename) `SAppV` iterateN (1 + inum) SLamV (Wildcard SType))
                     [ iterateN n SLamV $ guardTreeToCases $ Alts $ map (filterGuardTree (up n f) cn 0 n . upGT 0 n) ts
                     | (cn, n) <- cns
                     ]
@@ -713,6 +723,7 @@ compileGuardTree ulend lend adts t = (\x -> traceD ("  !  :" ++ ppShow x) x) $ g
     guardNode v [] e = e
     guardNode v [w] e = case w of
         PVar _ -> {-todo guardNode v (subst x v ws) $ -} varGuardNode 0 v e
+        PParens p -> guardNode v [p] e
         ViewPat f (ParPat p) -> guardNode (f `SAppV` v) p {- $ guardNode v ws -} e
         PCon (_, s) ps' -> GuardNode v s ps' {- $ guardNode v ws -} e
 
@@ -725,7 +736,7 @@ compileCase ge x cs
 -------------------------------------------------------------------------------- declaration representation
 
 data Stmt
-    = Let SIName MFixity (Maybe SExp) SExp
+    = Let SIName (Maybe SExp) SExp
     | Data SIName [(Visibility, SExp)]{-parameters-} SExp{-type-} Bool{-True:add foralls-} [(SIName, SExp)]{-constructor names and types-}
     | PrecDef SIName Fixity
 
@@ -737,7 +748,7 @@ data Stmt
     | FunAlt SIName [((Visibility, SExp), Pat)] (Either [(SExp, SExp)]{-guards-} SExp{-no guards-})
     deriving (Show)
 
-pattern Primitive n mf t <- Let n mf (Just t) (SBuiltin "undefined") where Primitive n mf t = Let n mf (Just t) $ SBuiltin "undefined"
+pattern Primitive n t <- Let n (Just t) (SBuiltin "undefined") where Primitive n t = Let n (Just t) $ SBuiltin "undefined"
 
 -------------------------------------------------------------------------------- declaration parsing
 
@@ -864,7 +875,7 @@ parseSomeGuards f = do
 mkLets :: DesugarInfo -> [Stmt]{-where block-} -> SExp{-main expression-} -> SExp{-big let with lambdas; replaces global names with de bruijn indices-}
 mkLets ds = mkLets' . sortDefs ds where
     mkLets' [] e = e
-    mkLets' (Let n _ mt x: ds) e
+    mkLets' (Let n mt x: ds) e
         = SLet n (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x') (substSG0 n $ mkLets' ds e)
       where
         x' = if usedS n x then SBuiltin "primFix" `SAppV` SLamV (substSG0 n x) else x
@@ -894,11 +905,11 @@ sortDefs ds xs = concatMap (desugarMutual ds) $ topSort mempty mempty mempty nod
     nodes = zip (zip [0..] xs) $ map (def &&& need) xs
     need = \case
         PrecDef{} -> mempty
-        Let _ _ mt e -> foldMap freeS' mt <> freeS' e
+        Let _ mt e -> foldMap freeS' mt <> freeS' e
         Data _ ps t _ cs -> foldMap (freeS' . snd) ps <> freeS' t <> foldMap (freeS' . snd) cs
     def = \case
         PrecDef{} -> mempty
-        Let n _ _ _ -> Set.singleton n
+        Let n _ _ -> Set.singleton n
         Data n _ _ _ cs -> Set.singleton n <> Set.fromList (map fst cs)
     freeS' = Set.fromList . freeS
     topSort acc@(_:_) defs vs xs | Set.null vs = reverse acc: topSort mempty defs vs xs
@@ -946,15 +957,15 @@ compileFunAlts compilegt ds xs = dsInfo >>= \ge -> case xs of
 --            , let ts = fst $ getParamsS $ up1 t
             , let as = [ FunAlt m p $ Right {- $ SLam Hidden (Wildcard SType) $ up1 -} $ SLet m' e $ SVar mempty 0
                       | Instance n' i cstrs alts <- ds, n' == n
-                      , Let m' ~Nothing ~Nothing e <- alts, m' == m
+                      , Let m' ~Nothing e <- alts, m' == m
                       , let p = zip ((,) Hidden <$> ps) i ++ [((Hidden, Wildcard SType), PVar (mempty, ""))]
         --              , let ic = sum $ map varP i
                       ]
             ]
         return $ cd ++ concat cds
-    [TypeAnn n t] -> return [Primitive n Nothing t | snd n `notElem` [n' | FunAlt (_, n') _ _ <- ds]]
+    [TypeAnn n t] -> return [Primitive n t | snd n `notElem` [n' | FunAlt (_, n') _ _ <- ds]]
     tf@[TypeFamily n ps t] -> case [d | d@(FunAlt n' _ _) <- ds, n' == n] of
-        [] -> return [Primitive n Nothing $ addParamsS ps t]
+        [] -> return [Primitive n $ addParamsS ps t]
         alts -> compileFunAlts compileGuardTrees' [TypeAnn n $ addParamsS ps t] alts
     [p@PrecDef{}] -> return [p]
     fs@(FunAlt n vs _: _) -> case map head $ group [length vs | FunAlt _ vs _ <- fs] of
@@ -963,7 +974,6 @@ compileFunAlts compilegt ds xs = dsInfo >>= \ge -> case xs of
           | n `elem` [n' | TypeFamily n' _ _ <- ds] -> return []
           | otherwise -> return
             [ Let n
-                (listToMaybe [t | PrecDef n' t <- ds, n' == n])
                 (listToMaybe [t | TypeAnn n' t <- ds, n' == n])
                 $ foldr (uncurry SLam . fst) (compilegt ge
                     [ compilePatts (zip (map snd vs) $ reverse [0.. num - 1]) gsx
@@ -984,7 +994,7 @@ mkDesugarInfo :: [Stmt] -> DesugarInfo
 mkDesugarInfo ss =
     ( Map.fromList $ ("'EqCTt", (Infix, -1)): [(s, f) | PrecDef (_, s) f <- ss]
     , Map.fromList $
-        [(cn, Left ((t, pars ty), (snd *** pars) <$> cs)) | Data (_, t) ps ty _ cs <- ss, ((_, cn), ct) <- cs]
+        [hackHList (cn, Left ((caseName t, pars ty), (snd *** pars) <$> cs)) | Data (_, t) ps ty _ cs <- ss, ((_, cn), ct) <- cs]
      ++ [(t, Right $ pars $ addParamsS ps ty) | Data (_, t) ps ty _ _ <- ss]
 --     ++ [(t, Right $ length xs) | Let (_, t) _ (Just ty) xs _ <- ss]
      ++ [("'Type", Right 0)]
@@ -992,6 +1002,10 @@ mkDesugarInfo ss =
   where
     pars ty = length $ filter ((== Visible) . fst) $ fst $ getParamsS ty -- todo
 
+    hackHList ("HCons", _) = ("HCons", Left (("hlistConsCase", 0), [("HCons", 2)]))
+    hackHList ("HNil", _) = ("HNil", Left (("hlistNilCase", 0), [("HNil", 0)]))
+    hackHList x = x
+
 joinDesugarInfo (fm, cm) (fm', cm') = (Map.union fm fm', Map.union cm cm')
 
 
@@ -1181,6 +1195,9 @@ isAtom' = (<=PrecAtom') . getPrec
 
 shAtom = PS PrecAtom
 shAtom' = PS PrecAtom'
+shTuple xs = prec PrecAtom $ \_ -> case xs of
+    [x] -> "((" ++ str x ++ "))"
+    xs -> "(" ++ intercalate ", " (map str xs) ++ ")"
 shAnn _ True x y | str y `elem` ["Type", inGreen "Type"] = x
 shAnn s simp x y | isAtom x && isAtom y = shAtom' $ str x <> s <> str y
 shAnn s simp x y = prec PrecAnn $ lpar x <> " " <> const s <> " " <> rpar y