Define kinds and monotypes.

3 files changed, 204 insertions, 0 deletions

diff --git a/src/Inky/Kind.idr b/src/Inky/Kind.idr
new file mode 100644
index 0000000..a09c97d
--- /dev/null
+++ b/src/Inky/Kind.idr
@@ -0,0 +1,50 @@
+module Inky.Kind
+
+import Control.Function
+import Data.Bool.Decidable
+import Decidable.Equality.Core
+
+public export
+data Kind : Type where
+  KStar : Kind
+  KArrow : Kind -> Kind -> Kind
+
+export
+Eq Kind where
+  KStar == KStar = True
+  (t1 `KArrow` u1) == (t2 `KArrow` u2) = t1 == t2 && u1 == u2
+  _ == _ = False
+
+export
+Uninhabited (KStar = KArrow t u) where
+  uninhabited prf impossible
+
+export
+Uninhabited (KArrow t u = KStar) where
+  uninhabited prf impossible
+
+export
+Biinjective KArrow where
+  biinjective Refl = (Refl, Refl)
+
+export
+DecEq Kind where
+  decEq KStar KStar = Yes Refl
+  decEq KStar (KArrow _ _) = No absurd
+  decEq (KArrow k1 k2) KStar = No absurd
+  decEq (KArrow k1 k2) (KArrow j1 j2) =
+    case (decEq k1 j1, decEq k2 j2) of
+      (Yes eq1, Yes eq2) => Yes (cong2 KArrow eq1 eq2)
+      (Yes eq1, No neq2) => No (neq2 . snd . biinjective)
+      (No neq1, _) => No (neq1 . fst . biinjective)
+
+export
+decEqReflects : (k, j : Kind) -> (k = j) `Reflects` (k == j)
+decEqReflects KStar KStar = RTrue Refl
+decEqReflects KStar (KArrow _ _) = RFalse absurd
+decEqReflects (KArrow k1 k2) KStar = RFalse absurd
+decEqReflects (KArrow k1 k2) (KArrow j1 j2) with (decEqReflects k1 j1) | (k1 == j1)
+  _ | RTrue eq1 | _ with (decEqReflects k2 j2) | (k2 == j2)
+    _ | RTrue eq2 | _ = RTrue (cong2 KArrow eq1 eq2)
+    _ | RFalse neq2 | _ = RFalse (neq2 . snd . biinjective)
+  _ | RFalse neq1 | _ = RFalse (neq1 . fst . biinjective)
diff --git a/src/Inky/OnlyWhen.idr b/src/Inky/OnlyWhen.idr
new file mode 100644
index 0000000..7bed91a
--- /dev/null
+++ b/src/Inky/OnlyWhen.idr
@@ -0,0 +1,44 @@
+module Inky.OnlyWhen
+
+import Data.DPair
+
+public export
+data OnlyWhen : Maybe a -> (a -> Type) -> Type where
+  Yes : forall x. (px : p x) -> Just x `OnlyWhen` p
+  No : ((x : a) -> Not (p x)) -> Nothing `OnlyWhen` p
+
+public export
+decDPair : (v **  v `OnlyWhen` p) <=> Dec (x : a ** p x)
+decDPair =
+  MkEquivalence
+    { leftToRight = \case
+      (Just x ** Yes px) => Yes (x ** px)
+      (Nothing ** No prf) => No (\(x ** px) => prf x px)
+    , rightToLeft = \case
+      Yes (x ** px) => (Just x ** Yes px)
+      No prf => (Nothing ** No (\x, px => prf (x ** px)))
+    }
+
+public export
+decExists : Exists (`OnlyWhen` p) <=> Dec (Exists p)
+decExists =
+  MkEquivalence
+    { leftToRight = \case
+      Evidence .(Just x) (Yes px) => Yes (Evidence x px)
+      Evidence .(Nothing) (No prf) => No (\(Evidence x px) => void (prf x px))
+    , rightToLeft = \case
+      Yes (Evidence x px) => Evidence (Just x) (Yes px)
+      No prf => Evidence Nothing (No (\x, px => prf (Evidence x px)))
+    }
+
+public export
+decSubset : Subset (Maybe a) (`OnlyWhen` p) <=> Dec (Subset a p)
+decSubset =
+  MkEquivalence
+    { leftToRight = \case
+      Element (Just x) prf => Yes (Element x (case prf of Yes px => px))
+      Element Nothing prf => No (\(Element x px) => void (case prf of No prf => prf x px))
+    , rightToLeft = \case
+      Yes (Element x px) => Element (Just x) (Yes px)
+      No prf => Element Nothing (No (\x, px => prf (Element x px)))
+    }
diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
new file mode 100644
index 0000000..8c4285e
--- /dev/null
+++ b/src/Inky/Type.idr
@@ -0,0 +1,110 @@
+module Inky.Type
+
+import Data.Bool.Decidable
+import Data.DPair
+import Inky.Binding
+import Inky.Env
+import Inky.Kind
+import Inky.OnlyWhen
+
+namespace Raw
+  public export
+  data RawSTy : World -> Type where
+
+  public export
+  data RawCTy : World -> Type where
+
+  data RawSTy where
+    TVar : (x : Name w) -> RawSTy w
+    TNat : RawSTy w
+    TArrow : RawCTy w -> RawCTy w -> RawSTy w
+    TApp : RawSTy w -> RawCTy w -> RawSTy w
+    TAnnot : RawCTy w -> Kind -> RawSTy w
+
+  data RawCTy where
+    TFix : (x : Binder) -> RawCTy (w :< x) -> RawCTy w
+    TEmbed : RawSTy w -> RawCTy w
+
+public export
+data SynthKind : Env Kind w -> RawSTy w -> Kind -> Type where
+public export
+data CheckKind : Env Kind w -> Kind -> RawCTy w -> Type where
+
+data SynthKind where
+  TVar : SynthKind env (TVar x) (lookup env x)
+  TNat : SynthKind env TNat KStar
+  TArrow : CheckKind env KStar t -> CheckKind env KStar u -> SynthKind env (t `TArrow` u) KStar
+  TApp : SynthKind env f (k `KArrow` j) -> CheckKind env k t -> SynthKind env (f `TApp` t) j
+  TAnnot : CheckKind env k t -> SynthKind env (TAnnot t k) k
+
+data CheckKind where
+  TFix : CheckKind (env :< (x :~ k)) k t -> CheckKind env k (TFix x t)
+  TEmbed : SynthKind env a j -> k = j -> CheckKind env k (TEmbed a)
+
+export
+synthKindUniq : SynthKind env t k -> SynthKind env t j -> k = j
+synthKindUniq TVar TVar = Refl
+synthKindUniq TNat TNat = Refl
+synthKindUniq (TArrow p1 p2) (TArrow p3 p4) = Refl
+synthKindUniq (TApp p1 p2) (TApp p3 p4) = case (synthKindUniq p1 p3) of Refl => Refl
+synthKindUniq (TAnnot p1) (TAnnot p2) = Refl
+
+export
+synthKind : (env : Env Kind w) -> (a : RawSTy w) -> Maybe Kind
+export
+checkKind : (env : Env Kind w) -> (k : Kind) -> (t : RawCTy w) -> Bool
+
+synthKind env (TVar x) = Just (lookup env x)
+synthKind env TNat = Just KStar
+synthKind env (TArrow t u) = do
+  guard (checkKind env KStar t)
+  guard (checkKind env KStar u)
+  Just KStar
+synthKind env (TApp f t) = do
+  dom `KArrow` cod <- synthKind env f
+    | _ => Nothing
+  guard (checkKind env dom t)
+  Just cod
+synthKind env (TAnnot t k) = do
+  guard (checkKind env k t)
+  Just k
+
+checkKind env k (TFix x t) = checkKind (env :< (x :~ k)) k t
+checkKind env k (TEmbed a) =
+  case synthKind env a of
+    Nothing => False
+    Just k' => k == k'
+
+export
+synthKindPrf : (env : Env Kind w) -> (a : RawSTy w) -> synthKind env a `OnlyWhen` SynthKind env a
+export
+checkKindPrf : (env : Env Kind w) -> (k : Kind) -> (t : RawCTy w) -> CheckKind env k t `Reflects` checkKind env k t
+
+synthKindPrf env (TVar x) = Yes TVar
+synthKindPrf env TNat = Yes TNat
+synthKindPrf env (TArrow t u) with (checkKindPrf env KStar t) | (checkKind env KStar t)
+  _ | RTrue tStar | _ with (checkKindPrf env KStar u) | (checkKind env KStar u)
+    _ | RTrue uStar | _ = Yes (TArrow tStar uStar)
+    _ | RFalse uUnstar | _ = No (\_ => \case TArrow _ uStar => uUnstar uStar)
+  _ | RFalse tUnstar | _ = No (\_ => \case TArrow tStar _ => tUnstar tStar)
+synthKindPrf env (TApp f t) with (synthKindPrf env f) | (synthKind env f)
+  _ | Yes fArrow | Just (KArrow dom cod) with (checkKindPrf env dom t) | (checkKind env dom t)
+    _ | RTrue uDom | _ = Yes (TApp fArrow uDom)
+    _ | RFalse uUndom | _ =
+      No (\_ => \case
+        TApp fKind uDom => case synthKindUniq fArrow fKind of
+          Refl => uUndom uDom)
+  _ | Yes fStar | Just KStar = No (\_ => \case TApp fArrow _ => absurd (synthKindUniq fStar fArrow))
+  _ | No fUnkind | Nothing = No (\_ => \case TApp fKind _ => void (fUnkind _ fKind))
+synthKindPrf env (TAnnot t k) with (checkKindPrf env k t) | (checkKind env k t)
+  _ | RTrue tKind | _ = Yes (TAnnot tKind)
+  _ | RFalse tUnkind | _ = No (\_ => \case TAnnot tKind => tUnkind tKind)
+
+checkKindPrf env k (TFix x t) with (checkKindPrf (env :< (x :~ k)) k t) | (checkKind (env :< (x :~ k)) k t)
+  _ | RTrue tKind | _ = RTrue (TFix tKind)
+  _ | RFalse tUnkind | _ = RFalse (\case TFix tKind => tUnkind tKind)
+checkKindPrf env k (TEmbed a) with (synthKindPrf env a) | (synthKind env a)
+  _ | Yes aKind | Just k' with (decEqReflects k k') | (k == k')
+    _ | RTrue eq | _ = RTrue (TEmbed aKind eq)
+    _ | RFalse neq | _ = RFalse (\case TEmbed aKind' eq => neq $ trans eq $ synthKindUniq aKind' aKind)
+  _ | No aUnkind | _ = RFalse (\case TEmbed aKind Refl => aUnkind _ aKind)