+{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Typing.Kind where
-import qualified Data.Kind as Kind
-import Data.Proxy
-import Data.Type.Equality
-import GHC.Exts (Constraint)
-import GHC.Prim (Any)
+import Data.Type.Equality (TestEquality(..), (:~:)(..))
+import qualified Data.Kind as K
--- * Type 'SKind'
+import Language.Symantic.Grammar
+
+-- * Type 'Kind'
-- | Singleton for kind types.
-data SKind k where
- SKiType :: SKind Kind.Type
- SKiConstraint :: SKind Constraint
- SKiArrow :: SKind ka -> SKind kb -> SKind (ka -> kb)
-infixr 5 `SKiArrow`
-
-instance Show (SKind k) where
- show SKiType = "*"
- show SKiConstraint = "Constraint"
- show (SKiArrow a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
-instance TestEquality SKind where
- testEquality = eq_skind
-
-eq_skind :: SKind x -> SKind y -> Maybe (x:~:y)
-eq_skind SKiType SKiType = Just Refl
-eq_skind SKiConstraint SKiConstraint = Just Refl
-eq_skind (SKiArrow xa xb) (SKiArrow ya yb)
- | Just Refl <- eq_skind xa ya
- , Just Refl <- eq_skind xb yb
+data Kind src k where
+ KiType :: src -> Kind src K.Type
+ KiConstraint :: src -> Kind src K.Constraint
+ KiFun :: src -> Kind src ka -> Kind src kb -> Kind src (ka -> kb)
+infixr 5 `KiFun`
+
+type instance SourceOf (Kind src k) = src
+instance Source src => Sourced (Kind src k) where
+ sourceOf (KiType src) = src
+ sourceOf (KiConstraint src) = src
+ sourceOf (KiFun src _a _b) = src
+
+ setSource (KiType _loc) src = KiType src
+ setSource (KiConstraint _loc) src = KiConstraint src
+ setSource (KiFun _loc a b) src = KiFun src a b
+
+instance Show (Kind src k) where
+ show KiType{} = "*"
+ show KiConstraint{} = "Constraint"
+ show (KiFun _src a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
+instance TestEquality (Kind src) where
+ testEquality = eqKind
+
+eqKind :: Kind xs x -> Kind ys y -> Maybe (x:~:y)
+eqKind KiType{} KiType{} = Just Refl
+eqKind KiConstraint{} KiConstraint{} = Just Refl
+eqKind (KiFun _xs xa xb) (KiFun _ys ya yb)
+ | Just Refl <- eqKind xa ya
+ , Just Refl <- eqKind xb yb
= Just Refl
-eq_skind _ _ = Nothing
+eqKind _ _ = Nothing
+
+-- * Type 'K'
+type K (t::kt) = kt
+
+-- * Class 'KindOf'
+-- | Return the 'Kind' of something.
+class KindOf (a::kt -> K.Type) where
+ kindOf :: a t -> Kind (SourceOf (a t)) kt
--- * Type 'IKind'
--- | Implicit 'SKind'.
+-- * Type 'Inj_Kind'
+-- | Implicit 'Kind'.
--
-- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
--- makes it fail to properly build an implicit 'SKind',
+-- makes it fail to properly build an implicit 'Kind',
-- this can however be worked around by having the class instances
--- work on a data type 'Ty' instead of 'Data.Kind.Type',
--- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'IKindP'.
-class (IKindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => IKind k where
- kind :: SKind k
- kind = kindP (Proxy @(Ty_of_Type k))
-instance (IKindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => IKind k
-
--- ** Type 'IKindP'
-class IKindP k where
- kindP :: Proxy k -> SKind (Type_of_Ty k)
-instance IKindP Constraint where
- kindP _ = SKiConstraint
-instance IKindP Ty where
- kindP _ = SKiType
-instance (IKindP a, IKindP b) => IKindP (a -> b) where
- kindP _ = kindP (Proxy @a) `SKiArrow` kindP (Proxy @b)
+-- work on a data type 'Ty' instead of 'Data.K.Type',
+-- hence the introduction of 'Ty', 'Ty_of_Type', 'Type_of_Ty' and 'Inj_KindP'.
+class (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k where
+instance (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k
+
+inj_Kind ::
+ forall k src.
+ Source src =>
+ Inj_Kind k =>
+ Kind src k
+inj_Kind = inj_KindP @(Ty_of_Type k) (noSource @src)
+
+-- ** Type 'Inj_KindP'
+class Inj_KindP k where
+ inj_KindP :: src -> Kind src (Type_of_Ty k)
+instance Inj_KindP K.Constraint where
+ inj_KindP = KiConstraint
+instance Inj_KindP Ty where
+ inj_KindP = KiType
+instance (Inj_KindP a, Inj_KindP b) => Inj_KindP (a -> b) where
+ inj_KindP src = KiFun src (inj_KindP @a src) (inj_KindP @b src)
-- ** Type 'Ty'
--- | FIXME: to be removed when
+-- | FIXME: workaround to be removed when
-- <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>
-- will be fixed.
data Ty
-- ** Type family 'Ty_of_Type'
-type family Ty_of_Type (typ::Kind.Type) :: Kind.Type
-type instance Ty_of_Type Kind.Type = Ty
-type instance Ty_of_Type Constraint = Constraint
-type instance Ty_of_Type (a -> b) = Ty_of_Type a -> Ty_of_Type b
+-- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here,
+-- this notably disables the expansion of 'Ty_of_Type'@ Any@.
+type family Ty_of_Type (t::K.Type) :: K.Type
+type instance Ty_of_Type K.Type = Ty
+type instance Ty_of_Type K.Constraint = K.Constraint
+type instance Ty_of_Type (a -> b) = Ty_of_Type a -> Ty_of_Type b
-- ** Type family 'Type_of_Ty'
-type family Type_of_Ty (typ::Kind.Type) :: Kind.Type
-type instance Type_of_Ty Ty = Kind.Type
-type instance Type_of_Ty Constraint = Constraint
-type instance Type_of_Ty (a -> b) = Type_of_Ty a -> Type_of_Ty b
+-- | NOTE: As of GHC-8.0.2, using a closed /type family/ does not work here,
+-- this notably disables the expansion of 'Type_of_Ty'@ Any@.
+type family Type_of_Ty (t::K.Type) :: K.Type
+type instance Type_of_Ty Ty = K.Type
+type instance Type_of_Ty K.Constraint = K.Constraint
+type instance Type_of_Ty (a -> b) = Type_of_Ty a -> Type_of_Ty b
--- * Type 'EKind'
+-- * Type 'KindK'
-- | Existential for 'Kind'.
-data EKind = forall k. EKind (SKind k)
-instance Eq EKind where
- EKind x == EKind y
- | Just _ <- eq_skind x y = True
+data KindK src = forall k. KindK (Kind src k)
+instance Eq (KindK src) where
+ KindK x == KindK y
+ | Just _ <- eqKind x y = True
_x == _y = False
-instance Show EKind where
- show (EKind x) = show x
-
--- * Type family 'Kind_Of'
-type family Kind_Of (x::k) :: Kind.Type
-type instance Kind_Of (x::Constraint) = Constraint
-type instance Kind_Of (x::Kind.Type) = Kind.Type
-type instance Kind_Of (x::a -> b) = Kind_Of (Any::a) -> Kind_Of (Any::b)
-
-{-
-instance Show (x :~~: y) where
- show _ = "HRefl"
-
-type family Eq_KindF (x::kx) (y::ky) :: Bool where
- Eq_KindF (x::k) (y::k) = 'True
- Eq_KindF x y = 'False
-
-type Eq_Kind x y = Eq_KindB (Eq_KindF x y) x y
-class Eq_KindB (b::Bool) (x::kx) (y::ky) where
- eq_kindB :: Proxy b -> Proxy x -> Proxy y -> Maybe (x:~~:y)
-instance Eq_KindB 'False x y where
- eq_kindB _b _x _y = Nothing
-instance Eq_KindB 'True (x::Kind.Type) (y::Kind.Type) where
- eq_kindB _b _x _y = Just HRefl
-instance Eq_KindB 'True (x::Constraint) (y::Constraint) where
- eq_kindB _b _x _y = Just HRefl
-instance
- ( Eq_Kind (Any::k0) (Any::k2)
- , Eq_Kind (Any::k1) (Any::k3)
- ) => Eq_KindB 'True (x::k0 -> k1) (y::k2 -> k3) where
- eq_kindB _b _x _y
- | Just HRefl <- eq_kind (Proxy @(Any::k0)) (Proxy @(Any::k2))
- , Just HRefl <- eq_kind (Proxy @(Any::k1)) (Proxy @(Any::k3))
- = Just HRefl
- eq_kindB _b _x _y = Nothing
-
-eq_kind :: forall x y. Eq_Kind x y => Proxy x -> Proxy y -> Maybe (x:~~:y)
-eq_kind = eq_kindB (Proxy @(Eq_KindF x y))
--}
+instance Show (KindK src) where
+ show (KindK x) = show x
+
+-- * Type 'Con_Kind'
+data Con_Kind src
+ = Con_Kind_Eq (KindK src) (KindK src)
+ | Con_Kind_Arrow (KindK src)
+ deriving (Eq, Show)
+
+when_EqKind
+ :: Inj_Error (Con_Kind src) err
+ => Kind src x
+ -> Kind src y
+ -> ((x :~: y) -> Either err ret) -> Either err ret
+when_EqKind x y k =
+ case x `eqKind` y of
+ Just Refl -> k Refl
+ Nothing -> Left $ inj_Error $ Con_Kind_Eq (KindK x) (KindK y)
+
+when_KiFun ::
+ Inj_Error (Con_Kind src) err =>
+ Inj_Source (KindK src) src =>
+ Kind src x ->
+ (forall a b. (x :~: (a -> b)) ->
+ Kind src a ->
+ Kind src b ->
+ Either err ret) ->
+ Either err ret
+when_KiFun x k =
+ case x of
+ KiFun _src a b -> k Refl (a `source` KindK x) (b `source` KindK x)
+ _ -> Left $ inj_Error $ Con_Kind_Arrow (KindK x)
sourcephile / git / haskell / symantic.git / blobdiff