refactoring

2 files changed, 15 insertions, 10 deletions

diff --git a/lc/Internals.lc b/lc/Internals.lc
index 15d1a38e..72386f16 100644
--- a/lc/Internals.lc
+++ b/lc/Internals.lc
@@ -13,6 +13,14 @@ data Unit = TT
 data String
 data Empty (a :: String)
 
+unsafeCoerce :: forall a b . a -> b
+
+-- equality constraints
+type family EqCT (t :: Type) (a :: t) (b :: t)
+{-
+coe :: forall (a :: Type) (b :: Type) -> EqCT Type a b -> a -> b
+coe a b TT x = unsafeCoerce @a @b x
+-}
 -- TODO: generate?
 data Tuple0 = Tuple0
 data Tuple1 a = Tuple1 a
@@ -39,16 +47,15 @@ type family T2 a b
 
 match'Type :: forall (m :: Type -> Type) -> m Type -> forall (t :: Type) -> m t -> m t
 
---testmt :: forall (t :: Type) -> t -> t
---testmt 'Type = \'Tuple0 -> 'Tuple0
-
--- equality constraints
-type family EqCT (t :: Type) (a :: t) (b :: t)
+testmt :: forall (t :: Type) -> t -> t
+testmt 'Type = \'Tuple0 -> 'Tuple0
+--testmt t x = (match'Type (\q -> (q -> q)) (\x -> match'Tuple0 (\q -> & 'Type) 'Tuple0 x undefined) t undefined) x
+--testmt t x = (match'Type (\q -> (q -> q)) (\x -> match'Tuple0 (\q -> 'Type) 'Tuple0 x undefined) t undefined) x
 
---type instance EqCT Type Type Type = Unit--(a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b')
---type instance EqCT Type (a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b')
+--type instance EqCT Type = \'Type 'Type -> 'Unit
+--type instance EqCT Type = \'(a, b) '(JoinTupleType a' b') -> '(T2 (EqCT Type a a') (EqCT Type b b'))
 
-type EqCTt = EqCT Type
+type EqCTt = EqCT _
 
 -- builtin conjuction of constraint witnesses
 t2C :: Unit -> Unit -> Unit
diff --git a/lc/Prelude.lc b/lc/Prelude.lc
index 167d5d05..b82cd903 100644
--- a/lc/Prelude.lc
+++ b/lc/Prelude.lc
@@ -125,8 +125,6 @@ type instance Split z (RecordC xs) (RecordC ys) | defined xs &&& defined ys = T2
 record :: [(String, Type)] -> Type
 --record xs = RecordCons ({- TODO: sortBy fst-} xs)
 -}
--- builtin
-unsafeCoerce :: forall a b . a -> b
 
 isKeyC _ _ [] = 'Empty ""
 isKeyC s t ((s', t'): ss) = if s == s' then t ~ t' else isKeyC s t ss