implement constraint kinds

6 files changed, 81 insertions, 81 deletions

diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs
index 377cd164..9fc61888 100644
--- a/src/LambdaCube/Compiler/Core.hs
+++ b/src/LambdaCube/Compiler/Core.hs
@@ -216,13 +216,14 @@ pattern TyConN s a <- TyCon (TyConName s _ _ _ _) a
 pattern TTyCon s t a <- TyCon (TyConName s _ t _ _) a
 pattern TFun' a t b = DFun (FunName' a t) b
 
-
-pattern TTyCon0 s  <- TyCon (TyConName s _ TType _ _) []
+pattern TTyCon0 s  <- TyCon (TyConName s _ _ _ _) []
 
 tTyCon s t a cs = TyCon (TyConName s (error "todo: inum") t (map ((,) (error "tTyCon")) cs) $ CaseFunName (error "TTyCon-A") (error "TTyCon-B") $ length a) a
 tTyCon0 s cs = Closed $ TyCon (TyConName s 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) []
+
 pattern a :~> b = Pi Visible a b
 
+pattern TConstraint <- TTyCon0 FConstraint where TConstraint = tTyCon0 FConstraint $ error "cs 1"
 pattern Unit        <- TTyCon0 FUnit      where Unit        = tTyCon0 FUnit [Unit]
 pattern TInt        <- TTyCon0 FInt       where TInt        = tTyCon0 FInt $ error "cs 1"
 pattern TNat        <- TTyCon0 FNat       where TNat        = tTyCon0 FNat $ error "cs 3"
@@ -233,8 +234,8 @@ pattern TChar       <- TTyCon0 FChar      where TChar       = tTyCon0 FChar $ er
 pattern TOrdering   <- TTyCon0 FOrdering  where TOrdering   = tTyCon0 FOrdering $ error "cs 8"
 pattern TVec a b    <- TyConN FVecS [b, a]
 
-pattern Empty s   <- TyCon (TyConName FEmpty _ _ _ _) [HString{-hnf?-} s] where
-        Empty s    = TyCon (TyConName FEmpty (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [HString s]
+pattern Empty s    <- TyCon (TyConName FEmpty _ _ _ _) [HString{-hnf?-} s]
+  where Empty s     = TyCon (TyConName FEmpty (error "todo: inum2_") (TString :~> TType) (error "todo: tcn cons 3_") $ error "Empty") [HString s]
 
 pattern TT          <- ConN' _ _
   where TT          =  Closed (tCon FTT 0 Unit [])
@@ -243,11 +244,17 @@ pattern Zero        <- ConN FZero _
 pattern Succ n      <- ConN FSucc (n:_)
   where Succ n      =  tCon FSucc 1 (TNat :~> TNat) [n]
 
+pattern CUnit       <- ConN FCUnit _
+  where CUnit       =  tCon FCUnit 0 TConstraint []
+pattern CEmpty s    <- ConN FCEmpty (HString s: _)
+  where CEmpty s    =  tCon FCEmpty 1 (TString :~> TConstraint) [HString s]
+
 pattern CstrT t a b     = Neut (CstrT' t a b)
-pattern CstrT' t a b    = TFun' FEqCT (TType :~> Var 0 :~> Var 1 :~> TType) [t, a, b]
-pattern Coe a b w x     = TFun Fcoe (TType :~> TType :~> CstrT TType (Var 1) (Var 0) :~> Var 2 :~> Var 2) [a,b,w,x]
+pattern CstrT' t a b    = TFun' FEqCT (TType :~> Var 0 :~> Var 1 :~> TConstraint) [t, a, b]
+pattern Coe a b w x     = TFun Fcoe (TType :~> TType :~> CW (CstrT TType (Var 1) (Var 0)) :~> Var 2 :~> Var 2) [a,b,w,x]
 pattern ParEval t a b   = TFun FparEval (TType :~> Var 0 :~> Var 1 :~> Var 2) [t, a, b]
-pattern T2 a b          = TFun FT2 (TType :~> TType :~> TType) [a, b]
+pattern T2 a b          = TFun FT2 (TConstraint :~> TConstraint :~> TConstraint) [a, b]
+pattern CW a            = TFun FCW (TConstraint :~> TType) [a]
 pattern CSplit a b c   <- UFunN FSplit [a, b, c]
 
 pattern HLit a <- (hnf -> ELit a)
@@ -422,7 +429,7 @@ instance Up Exp where
         Pi _ a b -> foldVar f i a <> foldVar f (i+1) b
         Con _ _ as -> foldMap (foldVar f i) as
         TyCon _ as -> foldMap (foldVar f i) as
-        TType -> mempty
+        TType_ _ -> mempty
         ELit{} -> mempty
         Neut x -> foldVar f i x
         Delta -> mempty
@@ -451,7 +458,7 @@ instance HasMaxDB Exp where
         Con_ c _ _ _ -> c
         TyCon_ c _ _ -> c
 
-        TType -> mempty
+        TType_ _ -> mempty
         ELit{} -> mempty
         Neut x -> maxDB_ x
         Delta -> mempty
@@ -484,7 +491,7 @@ instance ClosedExp Exp where
         Pi_ _ a b c -> Pi_ mempty a (closedExp b) c
         Con_ _ a b c -> Con_ mempty a b (closedExp <$> c)
         TyCon_ _ a b -> TyCon_ mempty a (closedExp <$> b)
-        e@TType{} -> e
+        e@TType_{} -> e
         e@ELit{} -> e
         Neut a -> Neut $ closedExp a
         Delta -> Delta
@@ -574,6 +581,7 @@ pattern FunName' a t <- FunName a _ t
 getFunDef s f = case show s of
     "'EqCT"             -> \case (t: a: b: _)   -> cstr t a b
     "'T2"               -> \case (a: b: _)      -> t2 a b
+    "'CW"               -> \case (a: _)         -> cw a
     "t2C"               -> \case (a: b: _)      -> t2C a b
     "coe"               -> \case (a: b: t: d: _) -> evalCoe a b t d
     "parEval"           -> \case (t: a: b: _)   -> parEval t a b
@@ -672,13 +680,13 @@ evalCoe a b (Reduced x) d = evalCoe a b x d
 evalCoe a b TT d = d
 evalCoe a b t d = Coe a b t d
 
-
+cstr_ t a b = cw $ cstr t a b
 
 cstr = f []
   where
     f z ty a a' = f_ z (hnf ty) (hnf a) (hnf a')
 
-    f_ _ _ a a' | a == a' = Unit
+    f_ _ _ a a' | a == a' = CUnit
     f_ ns typ (RHS a) (RHS 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'
@@ -687,17 +695,17 @@ cstr = f []
     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 (hnf -> UFunN FVecScalar [a, b]) (hnf -> UFunN FVecScalar [a', b']) = t2 (f [] TNat a a') (f [] TType b b')
-    f_ [] TType (hnf -> UFunN FVecScalar [a, b]) (TVec a' b') = t2 (f [] TNat a a') (f [] TType b b')
-    f_ [] TType (hnf -> UFunN FVecScalar [a, b]) t@NonNeut = t2 (f [] TNat a (ENat 1)) (f [] TType b t)
-    f_ [] TType (TVec a' b') (hnf -> UFunN FVecScalar [a, b]) = t2 (f [] TNat a' a) (f [] TType b' b)
-    f_ [] TType t@NonNeut (hnf -> UFunN FVecScalar [a, b]) = t2 (f [] TNat a (ENat 1)) (f [] TType b t)
+    f_ [] TType (UFunN FVecScalar [a, b]) (UFunN FVecScalar [a', b']) = t2 (f [] TNat a a') (f [] TType b b')
+    f_ [] TType (UFunN FVecScalar [a, b]) (TVec a' b') = t2 (f [] TNat a a') (f [] TType b b')
+    f_ [] TType (UFunN FVecScalar [a, b]) t@NonNeut = t2 (f [] TNat a (ENat 1)) (f [] TType b t)
+    f_ [] TType (TVec a' b') (UFunN FVecScalar [a, b]) = t2 (f [] TNat a' a) (f [] TType b' b)
+    f_ [] TType t@NonNeut (UFunN FVecScalar [a, b]) = 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_ ns typ a a' = Empty $ unlines [ "can not unify", ppShow a, "with", ppShow a' ]
+    f_ ns typ a a' = CEmpty $ unlines [ "can not unify", ppShow a, "with", ppShow a' ]
 
-    ff _ _ [] = Unit
+    ff _ _ [] = CUnit
     ff ns tt@(Pi v t _) ((t1, t2'): ts) = t2 (f ns t t1 t2') $ ff ns (appTy tt t1) ts
     ff ns t zs = error $ "ff: " -- ++ show (a, n, length xs', length $ mkConPars n typ) ++ "\n" ++ ppShow (nType a) ++ "\n" ++ ppShow (foldl appTy (nType a) $ mkConPars n typ) ++ "\n" ++ ppShow (zip xs xs') ++ "\n" ++ ppShow zs ++ "\n" ++ ppShow t
 
@@ -710,11 +718,15 @@ nonNeut _ = True
 t2C (hnf -> TT) (hnf -> TT) = TT
 t2C a b = TFun Ft2C (Unit :~> Unit :~> Unit) [a, b]
 
-t2 (hnf -> Unit) a = a
-t2 a (hnf -> Unit) = a
-t2 (hnf -> Empty a) (hnf -> Empty b) = Empty (a <> b)
-t2 (hnf -> Empty s) _ = Empty s
-t2 _ (hnf -> Empty s) = Empty s
+cw (hnf -> CUnit) = Unit
+cw (hnf -> CEmpty a) = Empty a
+cw a = CW a
+
+t2 (hnf -> CUnit) a = a
+t2 a (hnf -> CUnit) = a
+t2 (hnf -> CEmpty a) (hnf -> CEmpty b) = CEmpty (a <> b)
+t2 (hnf -> CEmpty s) _ = CEmpty s
+t2 _ (hnf -> CEmpty s) = CEmpty s
 t2 a b = T2 a b
 
 app_ :: Exp -> Exp -> Exp
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index 8f192c3c..271c678e 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -173,12 +173,10 @@ instance SetSourceInfo SIName where
 -- TODO: simplify this
 data FName
     = CFName !Int (SData SIName)
-    | FEqCT | FT2 | Fcoe | FparEval | Ft2C | FprimFix
-    | FType | FUnit | FInt | FWord | FNat | FBool | FFloat | FString | FChar | FOrdering | FVecS | FEmpty | FHList | FOutput
-    | FHCons | FHNil | FZero | FSucc | FFalse | FTrue | FLT | FGT | FEQ | FTT | FNil | FCons
+    | FEqCT | FT2 | Fcoe | FparEval | Ft2C | FprimFix | FCW
+    | FType | FConstraint | FUnit | FInt | FWord | FNat | FBool | FFloat | FString | FChar | FOrdering | FVecS | FEmpty | FHList | FOutput
+    | FHCons | FHNil | FZero | FSucc | FFalse | FTrue | FLT | FGT | FEQ | FTT | FNil | FCons | FCUnit | FCEmpty
     | FSplit | FVecScalar
-    -- todo: elim
-    | FEq | FOrd | FNum | FSigned | FComponent | FIntegral | FFloating
     deriving (Eq, Ord)
 
 mkFName' (RangeSI (Range fn p _)) s = fromMaybe (hashPos fn p) $ lookup s $ zipWith (\i (s, _) -> (s, i)) [0..] fntable
@@ -196,6 +194,10 @@ fntable =
     , (,) "coe"         Fcoe
     , (,) "parEval"     FparEval
     , (,) "t2C"         Ft2C
+    , (,) "'CW"         FCW
+    , (,) "'Constraint" FConstraint
+    , (,) "CEmpty"      FCEmpty
+    , (,) "CUnit"       FCUnit
     , (,) "primFix"     FprimFix
     , (,) "'Unit"       FUnit
     , (,) "'Int"        FInt
@@ -209,13 +211,6 @@ fntable =
     , (,) "'VecS"       FVecS
     , (,) "'Empty"      FEmpty
     , (,) "'HList"      FHList
-    , (,) "'Eq"         FEq
-    , (,) "'Ord"        FOrd
-    , (,) "'Num"        FNum
-    , (,) "'Signed"     FSigned
-    , (,) "'Component"  FComponent
-    , (,) "'Integral"   FIntegral
-    , (,) "'Floating"   FFloating
     , (,) "'Output"     FOutput
     , (,) "'Type"       FType
     , (,) "HCons"       FHCons
@@ -317,9 +312,11 @@ pattern ConsName <- SIName _ ":"
 pattern SRHS a      = SBuiltin "_rhs"     `SAppV` a
 pattern Section e   = SBuiltin "^section" `SAppV` e
 pattern SType       = SBuiltin "'Type"
+pattern SConstraint = SBuiltin "'Constraint"
 pattern Parens e    = SBuiltin "parens"   `SAppV` e
 pattern SAnn a t    = SBuiltin "typeAnn"  `SAppH` t `SAppV` a
 pattern TyType a    = SAnn a SType
+pattern SCW a       = SBuiltin "'CW"      `SAppV` a
 
 -- builtin heterogenous list
 pattern HList a   = SBuiltin "'HList" `SAppV` a
@@ -455,8 +452,7 @@ instance (Up a, PShow a) => PShow (SExp' a) where
         SGlobal ns      -> pShow ns
         Parens x        -> pShow x     -- TODO: remove
         SAnn a b        -> shAnn (pShow a) (pShow b)
-        TyType a        -> text "tyType" `dApp` pShow a
-        SAppV a b       -> pShow a `dApp` pShow b
+        TyType a        -> text "tyType" `DApp` pShow a
         SApp h a b      -> shApp h (pShow a) (pShow b)
         Wildcard SType  -> text "_"
         Wildcard t      -> shAnn (text "_") (pShow t)
@@ -472,6 +468,13 @@ shApp Hidden a b = DApp a (DAt b)
 
 shLam usedVar h a b = shLam_ usedVar h (Just a) b
 
+shLam_ False (BPi Hidden) (Just (DText "'CW" `DApp` a)) b = DFreshName False $ showContext (DUp 0 a) b
+  where
+    showContext x (DFreshName u d) = DFreshName u $ showContext (DUp 0 x) d
+    showContext x (DParContext xs y) = DParContext (DComma x xs) y
+    showContext x (DContext xs y) = DParContext (DComma x xs) y
+    showContext x y = DContext x y
+
 shLam_ usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 <$> a) b
   where
     lam = case h of
@@ -497,6 +500,7 @@ shLam_ usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 <$> a) b
     showForall s x (DForall s' xs y) | s == s' = DForall s (DSep (InfixR 11) x xs) y
     showForall s x y = DForall s x y
 
+    -- TODO: use other sign instead of (=>)
     showContext x (DFreshName u d) = DFreshName u $ showContext (DUp 0 x) d
     showContext x (DParContext xs y) = DParContext (DComma x xs) y
     showContext x (DContext xs y) = DParContext (DComma x xs) y
@@ -522,7 +526,7 @@ instance PShow Stmt where
     pShow stmt = vcat . map DResetFreshNames $ case stmt of
         Primitive n t -> pure $ shAnn (pShow n) (pShow t)
         Let n ty e -> [shAnn (pShow n) (pShow t) | Just t <- [ty]] ++ [DLet "=" (pShow n) (pShow e)]
-        Data n ps ty cs -> pure $ nest 2 $ "data" <+> nest 2 (shAnn (foldl dApp (DTypeNamespace True $ pShow n) [shAnn (text "_") (pShow t) | (v, t) <- ps]) (pShow ty)) </> "where" <> nest 2 (hardline <> vcat [shAnn (pShow n) $ pShow $ UncurryS (first (const Hidden) <$> ps) t | (n, t) <- cs])
+        Data n ps ty cs -> pure $ nest 2 $ "data" <+> nest 2 (shAnn (foldl DApp (DTypeNamespace True $ pShow n) [shAnn (text "_") (pShow t) | (v, t) <- ps]) (pShow ty)) </> "where" <> nest 2 (hardline <> vcat [shAnn (pShow n) $ pShow $ UncurryS (first (const Hidden) <$> ps) t | (n, t) <- cs])
         PrecDef n i -> pure $ pShow i <+> text (sName n) --DOp0 (sName n) i
 
 instance DeBruijnify SIName Stmt where
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 5ff71a52..6b2bece3 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -86,20 +86,20 @@ showEnvSExp :: (PShow a, Up a) => Env -> SExp' a -> String
 showEnvSExp e c = show $ envDoc e $ underline $ pShow c
 
 showEnvSExpType :: (PShow a, Up a) => Env -> SExp' a -> Exp -> String
-showEnvSExpType e c t = show $ envDoc e $ underline $ (shAnn (pShow c) (mkDoc False (ET t TType)))
+showEnvSExpType e c t = show $ envDoc e $ underline $ (shAnn (pShow c) (mkDoc False t))
 
 envDoc :: Env -> Doc -> Doc
 envDoc x m = case x of
     EGlobal{}           -> m
     EBind1 _ h ts b     -> envDoc ts $ shLam (usedVar 0 b) h m (pShow b)
-    EBind2 h a ts       -> envDoc ts $ shLam True h (mkDoc False (ET a TType)) m
+    EBind2 h a ts       -> envDoc ts $ shLam True h (mkDoc False a) m
     EApp1 _ h ts b      -> envDoc ts $ shApp h m (pShow b)
     EApp2 _ h (ET (Lam (Var 0)) (Pi Visible TType _)) ts -> envDoc ts $ shApp h (text "tyType") m
     EApp2 _ h a ts      -> envDoc ts $ shApp h (mkDoc False a) m
     ELet1 _ ts b        -> envDoc ts $ shLet_ m (pShow b)
     ELet2 _ x ts        -> envDoc ts $ shLet_ (mkDoc False x) m
     EAssign i x ts      -> envDoc ts $ shLet i (mkDoc False x) m
-    CheckType t ts      -> envDoc ts $ shAnn m $ mkDoc False (ET t TType)
+    CheckType t ts      -> envDoc ts $ shAnn m $ mkDoc False t
     CheckIType t ts     -> envDoc ts $ shAnn m (text "??") -- mkDoc ts' t
 --    CheckSame t ts      -> envDoc ts $ shCstr <$> m <*> mkDoc ts' t
     CheckAppType si h t te b -> envDoc (EApp1 si h (CheckType_ (sourceInfo b) t te) b) m
@@ -149,7 +149,7 @@ instance (Subst Exp a, Rearrange a) => Subst Exp (CEnv a) where
             | j > i, Just x' <- down (j-1) x   -> assign (j-1) (subst i x' a) (subst i x' b)
             | j < i, Just a' <- down (i-1) a   -> assign j a' (subst (i-1) (subst j (expr a') x) b)
             | j < i, Just x' <- down j x       -> assign j (subst (i-1) x' a) (subst (i-1) x' b)
-            | j == i    -> Meta (cstr (ty a) x $ expr a) $ up1_ 0 b
+            | j == i                           -> Meta (cstr_ (ty a) x $ expr a) $ up1_ 0 b
 
 --swapAssign :: (Int -> Exp -> CEnv Exp -> a) -> (Int -> Exp -> CEnv Exp -> a) -> Int -> Exp -> CEnv Exp -> a
 swapAssign _ clet i (ET (Var j) t) b | i > j = clet j (ET (Var (i-1)) t) $ subst j (Var (i-1)) $ up1_ i b
@@ -338,7 +338,6 @@ inferN_ tellTrace = infer  where
         return $ ex == y
 -}
     checkSame te (Wildcard _) a = True
-    checkSame te (SGlobal (sName -> "'Type")) TType = True
     checkSame te SType TType = True
     checkSame te (SBind_ _ BMeta _ SType (STyped (ET (Var 0) _))) a = True
     checkSame te a b = error $ "checkSame: " ++ ppShow (a, b)
@@ -356,7 +355,7 @@ inferN_ tellTrace = infer  where
         CheckAppType si h t te b   -- App1 h (CheckType t te) b
             | Pi h' x (down 0 -> Just y) <- et, h == h' -> case t of
                 Pi Hidden t1 t2 | h == Visible -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet  -- <<e>> b : {t1} -> {t2}
-                _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr TType t y) $ EApp1 si h te b) $ up 1 eet
+                _ -> focus_ (EBind2_ (sourceInfo b) BMeta (cstr_ TType t y) $ EApp1 si h te b) $ up 1 eet
             | otherwise -> focus_ (EApp1 si h (CheckType_ (sourceInfo b) t te) b) eet
         EApp1 si h te b
             | Pi h' x y <- et, h == h' -> checkN (EApp2 si h eet te) b x
@@ -365,7 +364,7 @@ inferN_ tellTrace = infer  where
 --            | CheckAppType Hidden _ te' _ <- te -> error "ok"
             | otherwise -> infer (CheckType_ (sourceInfo b) (Var 2) $ cstr' h (up 2 et) (Pi Visible (Var 1) (Var 1)) (up 2 e) $ EBind2_ (sourceInfo b) BMeta TType $ EBind2_ (sourceInfo b) BMeta TType te) (up 3 b)
           where
-            cstr' h x y e = EApp2 mempty h (ET (evalCoe (up 1 x) (up 1 y) (Var 0) (up 1 e)) (up 1 y)) . EBind2_ (sourceInfo b) BMeta (cstr TType x y)
+            cstr' h x y e = EApp2 mempty h (ET (evalCoe (up 1 x) (up 1 y) (Var 0) (up 1 e)) (up 1 y)) . EBind2_ (sourceInfo b) BMeta (cstr_ TType x y)
         ELet2 ln (ET x{-let-} xt) te -> focus_ te $ subst 0 (mkELet ln x xt){-let-} eet{-in-}
         CheckIType x te -> checkN te x e
         CheckType_ si t te
@@ -373,7 +372,7 @@ inferN_ tellTrace = infer  where
                             -> focus_ (EApp1 mempty Hidden (CheckType_ si t te) $ Wildcard $ Wildcard SType) eet
             | hArgs et < hArgs t, Pi Hidden t1 t2 <- t
                             -> focus_ (CheckType_ si t2 $ EBind2 (BLam Hidden) t1 te) eet
-            | otherwise    -> focus_ (EBind2_ si BMeta (cstr TType t et) te) $ up 1 eet
+            | otherwise    -> focus_ (EBind2_ si BMeta (cstr_ TType t et) te) $ up 1 eet
         EApp2 si h (ET a at) te    -> focusTell te si $ ET (app_ a e) (appTy at e)        --  h??
         EBind1 si h te b   -> infer (EBind2_ (sourceInfo b) h e te) b
         EBind2_ si (BLam h) a te -> focus_ te $ lamPi h a eet
@@ -386,13 +385,14 @@ inferN_ tellTrace = infer  where
         ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-}
         EBind2_ si BMeta tt_ te
             | ERHS te'   <- te -> refocus (ERHS $ EBind2_ si BMeta tt_ te') eet
-            | (hnf -> Unit) <- tt    -> refocus te $ subst 0 TT eet
+            | Unit <- tt    -> refocus te $ subst 0 TT eet
+--            | CW (hnf -> CUnit) <- tt -> error "okk"--, let te' = EBind2_ si BMeta (up 1 $ cw y) $ EBind2_ si BMeta (cw x) te
             | Empty msg <- tt -> throwError' $ ETypeError (text msg) si
-            | T2 x y <- tt, let te' = EBind2_ si BMeta (up 1 y) $ EBind2_ si BMeta x te
+            | CW (hnf -> T2 x y) <- tt, let te' = EBind2_ si BMeta (up 1 $ cw y) $ EBind2_ si BMeta (cw x) te
                             -> refocus te' $ subst 2 (t2C (Var 1) (Var 0)) $ up 2 eet
-            | CstrT t a b <- tt, Just r <- cst (ET a t) b -> r
-            | CstrT t a b <- tt, Just r <- cst (ET b t) a -> r
-            | isCstr tt, EBind2 h x te' <- te{-, h /= BMeta todo: remove-}, Just x' <- down 0 tt, x == x'
+            | CW (hnf -> CstrT t a b) <- tt, Just r <- cst (ET a t) b -> r
+            | CW (hnf -> CstrT t a b) <- tt, Just r <- cst (ET b t) a -> r
+            | CW _ <- tt, EBind2 h x te' <- te, Just x' <- down 0 tt, x == x'
                             -> refocus te $ subst 1 (Var 0) eet
             | EBind2_ si' h x te' <- te, h /= BMeta, Just b' <- down 0 tt
                             -> refocus (EBind2_ si' h (up 1 x) $ EBind2_ si BMeta b' te') $ subst 2 (Var 0) $ up 1 eet
@@ -467,14 +467,9 @@ lamPi h t (ET x y) = ET (Lam x) (Pi h t y)
 
 replaceMetas bind = \case
     Meta a t -> bind a $ replaceMetas bind t
-    Assign i x t | x' <- up1_ i x -> bind (cstr (ty x') (Var i) $ expr x') . up 1 . up1_ i $ replaceMetas bind t
+    Assign i x t | x' <- up1_ i x -> bind (cstr_ (ty x') (Var i) $ expr x') . up 1 . up1_ i $ replaceMetas bind t
     MEnd t ->  t
 
-
-isCstr CstrT{} = True
-isCstr (UFunN s [_]) = s `elem` [FEq, FOrd, FNum, FSigned, FComponent, FIntegral, FFloating]       -- todo: use Constraint type to decide this
-isCstr _ = {- trace_ (ppShow c ++ show c) $ -} False
-
 -------------------------------------------------------------------------------- re-checking
 
 type Message = String
@@ -570,7 +565,7 @@ dependentVars ie = cycle mempty
 
     grow = flip foldMap ie $ \case
       (n, t) -> (Set.singleton n <-> freeVars t) <> case t of
-        CstrT _{-todo-} ty f -> freeVars ty <-> freeVars f
+        (hnf -> CW (hnf -> CstrT _{-todo-} ty f)) -> freeVars ty <-> freeVars f
         (hnf -> CSplit a b c) -> freeVars a <-> (freeVars b <> freeVars c)
         _ -> mempty
       where
@@ -746,12 +741,6 @@ lamify t x = addLams (fst $ getParams t) $ x $ downTo 0 $ arity t
 arity :: Exp -> Int
 arity = length . fst . getParams
 
-{-
-getApps' = second reverse . run where
-  run (App a b) = second (b:) $ run a
-  run x = (x, [])
--}
-
 inferTerm :: Monad m => String -> SExp2 -> IM m ExpType
 inferTerm msg t =
     fmap (closedExp . recheck msg EGlobal . replaceMetas (lamPi Hidden)) $ inferN EGlobal t
@@ -767,13 +756,9 @@ addToEnv sn@(SIName si s) (ET x t) = do
     case v of
       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
--}
 
 downTo n m = map Var [n+m-1, n+m-2..n]
 
-tellType si t = tell $ mkInfoItem (sourceInfo si) $ DTypeNamespace True $ mkDoc False (ET t TType)
+tellType si t = tell $ mkInfoItem (sourceInfo si) $ DTypeNamespace True $ mkDoc False t
 
 
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index eee794f9..cd118768 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -187,10 +187,8 @@ parseTermLam =
   where
     mkIf b t f = SBuiltin "primIfThenElse" `SAppV` b `SAppV` t `SAppV` f
 
-    mkPi Hidden xs b = foldr (sNonDepPi Hidden) b $ getTTuple xs
-    mkPi h a b = sNonDepPi h a b
-
-    sNonDepPi h a b = SPi h a $ up1 b
+    mkPi Hidden xs b = foldr (\a b -> SPi Hidden a $ up1 b) b $ map SCW $ getTTuple xs
+    mkPi Visible a b = SPi Visible a $ up1 b
 
 parseTermAnn = level parseTermOp $ \t -> SAnn t <$> parseType Nothing
 
@@ -423,7 +421,7 @@ parseDef =
             return $ pure $ Class x (map snd ts) cs
  <|> do reserved "instance" *> do
           typeNS $ do
-            constraints <- option [] $ try_ "constraint" $ getTTuple <$> setR parseTermOp <* reservedOp "=>"
+            constraints <- option [] $ try_ "constraint" $ map SCW . getTTuple <$> setR parseTermOp <* reservedOp "=>"
             x <- upperCase
             (nps, args) <- telescopePat
             cs <- expNS $ option [] $ reserved "where" *> identation False ({-deBruijnify nps <$> -} funAltDef (Just lhsOperator) varId)
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index c2651cba..f9702b94 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -311,8 +311,6 @@ pattern DArr x y = DArr_ "->" x y
 braces = DBrace
 parens = DParen
 
-dApp x y = DApp x y
-
 shCstr = DCstr
 
 shTuple [] = "()"
@@ -338,6 +336,9 @@ class PShow a where
 ppShow :: PShow a => a -> String
 ppShow = show . pShow
 
+tracePShow :: PShow a => a -> b -> b
+tracePShow a b = trace (ppShow a) b
+
 instance PShow Doc     where pShow = id
 instance PShow Int     where pShow = fromString . show
 instance PShow Integer where pShow = fromString . show
diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs
index 0046eb27..42f02b07 100644
--- a/src/LambdaCube/Compiler/Statements.hs
+++ b/src/LambdaCube/Compiler/Statements.hs
@@ -86,12 +86,12 @@ compileStmt compilegt ds = \case
     [Instance{}] -> return []
     [Class n ps ms] -> do
         cd <- compileStmt' $
-            [ TypeAnn n $ foldr (SPi Visible) SType ps ]
-         ++ [ funAlt n (map noTA ps) $ noGuards $ foldr (SAppV2 $ SBuiltin "'T2") (SBuiltin "'Unit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ]
-         ++ [ funAlt n (replicate (length ps) (noTA $ PVarSimp $ dummyName "cst0")) $ noGuards $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ sName n ++ " on ???"{-TODO-})]
+            [ TypeAnn n $ foldr (SPi Visible) SConstraint ps ]
+         ++ [ funAlt n (map noTA ps) $ noGuards $ foldr (SAppV2 $ SBuiltin "'T2") (SBuiltin "'CUnit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ]
+         ++ [ funAlt n (replicate (length ps) (noTA $ PVarSimp $ dummyName "cst0")) $ noGuards $ SBuiltin "'CEmpty" `SAppV` sLit (LString $ "no instance of " ++ sName n ++ " on ???"{-TODO-})]
         cds <- sequence
             [ compileStmt'_ SRHS SRHS{-id-}
-            $ TypeAnn m (UncurryS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS "a2" 0 $ length ps) $ up1 t)
+            $ TypeAnn m (UncurryS (map ((,) Hidden) ps) $ SPi Hidden (SCW $ foldl SAppV (SGlobal n) $ downToS "a2" 0 $ length ps) $ up1 t)
             : as
             | (m, t) <- ms
 --            , let ts = fst $ getParamsS $ up1 t