implement constraint kinds

3 files changed, 21 insertions, 22 deletions

diff --git a/lc/Builtins.lc b/lc/Builtins.lc
index 0ff2f3b1..03970dbd 100644
--- a/lc/Builtins.lc
+++ b/lc/Builtins.lc
@@ -489,9 +489,9 @@ rasterizePrimitives ctx is s = concat (map (rasterizePrimitive is ctx) s)
 
 type family ImageLC a :: Nat where ImageLC (Image n t) = n
 
-allSame :: [a] -> Type
-allSame [] = 'Unit
-allSame [x] = 'Unit
+allSame :: [a] -> Constraint
+allSame [] = 'CUnit
+allSame [x] = 'CUnit
 allSame (x: y: xs) = 'T2 (x ~ y) (allSame (y:xs))
 
 sameLayerCounts a = allSame (map 'ImageLC a)
diff --git a/lc/Internals.lc b/lc/Internals.lc
index 170f2c39..d8a08a33 100644
--- a/lc/Internals.lc
+++ b/lc/Internals.lc
@@ -18,8 +18,17 @@ data Empty (a :: String)
 
 unsafeCoerce :: forall a b . a -> b
 
+data Constraint where
+    CUnit :: Constraint
+    CEmpty :: String -> Constraint
+
+type family CW (c :: Constraint) -- where
+{-
+    CW 'CUnit = Unit
+    CW ('CEmpty s) = Empty s
+-}
 -- equality constraints
-type family EqCT (t :: Type) (a :: t) (b :: t)
+type family EqCT (t :: Type) (a :: t) (b :: t) :: Constraint
 {-
 coe :: forall (a :: Type) (b :: Type) -> EqCT Type a b -> a -> b
 coe a b TT x = unsafeCoerce @a @b x
@@ -31,7 +40,12 @@ coe a b TT x = unsafeCoerce @a @b x
 parEval :: forall a -> a -> a -> a
 
 -- conjuction of constraints
-type family T2 a b
+type family T2 (x :: Constraint) (y :: Constraint) :: Constraint
+{-
+type instance T2 'CUnit c = c
+type instance T2 c 'CUnit = c
+type instance T2 ('CEmpty s) ('CEmpty s') = 'CEmpty (s {- ++ s' TODO-})
+-}
 
 match'Type :: forall (m :: Type -> Type) -> m Type -> forall (t :: Type) -> m t -> m t
 
@@ -136,18 +150,4 @@ hlistConsCase
     -> c
 
 {-
--- TODO: unsafeCoerce is not really needed here
-hlistConsCase @e @f c fv x = 'HListCase 
-    (\_ _ -> c)
-    undefined
-    (\ @t @lt y ys -> fv (unsafeCoerce @t @e y) (unsafeCoerce @(HList lt) @(HList f) ys))
-    x
-
-hlistNilCase c x v = 'HListCase
-    (\_ _ -> c)
-    x
-    (\_ _ -> undefined :: c)
-    v
 -}
-
-
diff --git a/lc/Prelude.lc b/lc/Prelude.lc
index aa065096..5446df0d 100644
--- a/lc/Prelude.lc
+++ b/lc/Prelude.lc
@@ -126,7 +126,7 @@ recItemType (RecItem _ t) = t
 data RecordC (xs :: [RecItem])
     = RecordCons (HList (map recItemType xs))
 
-isKeyC _ _ [] = 'Empty ""
+isKeyC _ _ [] = 'CEmpty ""
 isKeyC s t (RecItem s' t': ss) = if s == s' then t ~ t' else isKeyC s t ss
 
 fstTup = hlistConsCase _ (\a _ -> a)
@@ -135,7 +135,7 @@ sndTup = hlistConsCase _ (\_ a -> a)
 -- todo: don't use unsafeCoerce
 project :: forall a (xs :: [RecItem]) . forall (s :: String) -> isKeyC s a xs => RecordC xs -> a
 project @a @('RecItem s' a': xs) s @_ (RecordCons ts) | s == s' = fstTup (unsafeCoerce @_ @(HList '(a : map recItemType xs)) ts)
-project @a @('RecItem s' a': xs) s @_ (RecordCons ts) = project @a @xs s @(undefined @(isKeyC s a xs)) (RecordCons (sndTup (unsafeCoerce @_ @(HList '(a : map recItemType xs)) ts)))
+project @a @('RecItem s' a': xs) s @_ (RecordCons ts) = project @a @xs s @(undefined @(CW (isKeyC s a xs))) (RecordCons (sndTup (unsafeCoerce @_ @(HList '(a : map recItemType xs)) ts)))
 
 --------------------------------------- HTML colors
 
@@ -388,4 +388,3 @@ fromTo a b
 (x : _)  !! 0  =  x
 (_ : xs) !! n  =  xs !! (n-1)
 
-