systemqfw

commit d23e713b8fd81d2edd633ad3f6554ae88a3c7a07
parent 1816e42deb15b5e96fa68e235f2acdbb9d70b32a
Author: Robert Russell <robert@rr3.xyz>
Date:   Wed, 28 Aug 2024 23:09:02 -0700

Add a coercion from kind * to kind $* to reduce verbosity

Diffstat:
M
Algebra.hs
 | 
4
+++-
M
Main.hs
 | 
10
+++++++---
M
Qul.hs
 | 
2
++
M
Qular.hs
 | 
2
++

4 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/Algebra.hs b/Algebra.hs
@@ -43,9 +43,11 @@ class Eq a => PartialOrd a where
 
     {-# MINIMAL pcompare | (?<) #-}
 
+{-
 class LubMonoid a where
     bot :: a
     (<^>) :: a -> a -> a
+-}
 
 class AddMonoid a where
     zero :: a
@@ -59,7 +61,7 @@ class MulScalar (MulActionScalar a) => MulAction a where
 
 class (
         PartialOrd a,
-        LubMonoid a,
+        -- LubMonoid a,
         AddMonoid a,
         MulAction a,
         MulActionScalar a ~ a
diff --git a/Main.hs b/Main.hs
@@ -136,8 +136,12 @@ checkType a k = case (a, k) of
         bindAndAssignType x dom \_ -> checkType body cod
     (a, k) -> do
         (a', k') <- inferType a
-        unless (k' == k) $ throwError ErrTypeInferCheckMismatch
-        pure a'
+        if k' == KindT && k == KindQT then
+            -- Coerce from kind * to kind $*
+            pure $ C.TypeQTPair (C.TypeQ defaultQuantity) a'
+        else do
+            unless (k' == k) $ throwError ErrTypeInferCheckMismatch
+            pure a'
 
 --------------------------------------------------------------------------------
 -- Term-level elaboration
@@ -235,7 +239,7 @@ checkTerm t q a = case (t, a) of
 --------------------------------------------------------------------------------
 
 input :: ByteString
-input = "\\[M] z s => z : @M : * -> top ! (top ! M -> top ! (top ! (top ! M -> top ! M) -> top ! M))"
+input = "\\[M] z s => z : @M:* -> M -> (M -> M) -> M"
 
 main :: IO ()
 main =
diff --git a/Qul.hs b/Qul.hs
@@ -21,12 +21,14 @@ instance PartialOrd Qul where
     _ ?< Omega = True
     _ ?< _ = False
 
+{-
 instance LubMonoid Qul where
     bot = Alpha
 
     Alpha <^> y = y
     x <^> Alpha = x
     x <^> y = if x == y then x else Omega
+-}
 
 -- Addition table:
 --     + │ α 0 1 ω
diff --git a/Qular.hs b/Qular.hs
@@ -24,6 +24,7 @@ instance PartialOrd Qular where
     One ?< Rel = True
     _ ?< _ = False
 
+{-
 instance LubMonoid Qular where
     bot = Alpha
 
@@ -34,6 +35,7 @@ instance LubMonoid Qular where
     Zero <^> One = Aff
     One <^> Zero = Aff
     x <^> y = fromMaybe Omega $ x `pmax` y
+-}
 
 -- Addition table:
 --     + │ α 0 1 A R ω