src/Symantic/Typer/Type.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE PatternSynonyms #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE RankNTypes #-}
   5 {-# LANGUAGE StandaloneDeriving #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 {-# LANGUAGE UndecidableSuperClasses #-}
   8 {-# LANGUAGE ViewPatterns #-}
   9 {-# OPTIONS_GHC -Wno-partial-fields #-}
  10
  11 module Symantic.Typer.Type where
  12
  13 import Control.Monad.Classes as MC ()
  14 import Control.Monad.Classes.Run as MC ()
  15 import Data.Eq (Eq (..))
  16 import Data.Function (($), (.))
  17 import Data.Functor ((<$>))
  18 import Data.Map.Strict qualified as Map
  19 import Data.Maybe (Maybe (..), isJust)
  20 import Data.Monoid (Monoid (..))
  21 import Data.Proxy (Proxy (..))
  22 import Data.Semigroup (Semigroup (..))
  23 import Data.String (String)
  24 import GHC.Types
  25 import Text.Show (Show (..))
  26 import Type.Reflection (TypeRep, Typeable, eqTypeRep, typeRep, typeRepKind, (:~~:) (..), pattern App)
  27 import Prelude (error)
  28 import Prelude qualified
  29
  30 import Symantic.Typer.Eq
  31 import Symantic.Typer.List
  32
  33 data Const meta (a :: aK) = Const
  34   { constType :: TypeRep a
  35   , constMeta :: meta
  36   }
  37   deriving (Show)
  38 instance EqTy (Const meta) (Const meta) where
  39   eqTy Const{constType = x} Const{constType = y} = eqTypeRep x y
  40
  41 type Name = String
  42
  43 -- * Type 'Var'
  44 data Var :: forall vK. Type -> [Type] -> vK -> Type where
  45   VarZ ::
  46     { varZKind :: Kind meta vK
  47     , varZNext :: Len ws
  48     , varZMeta :: meta
  49     } ->
  50     Var meta (Proxy (v :: vK) ': ws) (v :: vK)
  51   VarS :: Var meta vs v -> Var meta (not_v ': vs) v
  52 deriving instance Show meta => Show (Var meta vs v)
  53
  54 pattern Var :: () => () => Kind meta vK -> Len ws -> meta -> Var meta vs' (v :: vK)
  55 pattern Var{varKind, varNext, varMeta} <- (var -> VarVS VarZ{varZKind = varKind, varZNext = varNext, varZMeta = varMeta})
  56 {-# COMPLETE Var #-}
  57
  58 -- -- * Type 'VarVS'
  59 data VarVS meta (v :: vK) = forall vs. VarVS (Var meta vs v)
  60 var :: Var meta vs (v :: vK) -> VarVS meta (v :: vK)
  61 var v@VarZ{} = VarVS v
  62 var (VarS v) = var v
  63
  64 instance EqTy (Var meta vs) (Var meta vs) where
  65   eqTy VarZ{} VarZ{} = Just HRefl
  66   eqTy (VarS x) (VarS y) = eqTy x y
  67   eqTy _ _ = Nothing
  68
  69 type VarSem = Type -> [Type] -> Type -> Type
  70
  71 -- data VarV (var::VarSem) vs = forall vK (v::vK). VarVSem (var vs v)
  72 data VarV meta vs = forall v. VarV (Var meta vs v)
  73
  74 class LenVar var where
  75   lenVar :: var meta vs a -> Len vs
  76 instance LenVar Var where
  77   lenVar VarZ{varZNext} = LenS varZNext
  78   lenVar (VarS v) = LenS (lenVar v)
  79
  80 class LenVar var => AllocVars var where
  81   allocVarsL :: Len len -> var meta vs x -> var meta (len ++ vs) x
  82   allocVarsR :: Len len -> var meta vs x -> var meta (vs ++ len) x
  83 instance AllocVars Var where
  84   allocVarsL LenZ v = v
  85   allocVarsL (LenS len) v = VarS (allocVarsL len v)
  86
  87   allocVarsR len VarZ{..} = VarZ{varZNext = addLen varZNext len, ..}
  88   allocVarsR len (VarS v) = VarS (allocVarsR len v)
  89
  90 appendVars ::
  91   AllocVars xVar =>
  92   AllocVars yVar =>
  93   xVar meta xVS (x :: xK) ->
  94   yVar meta yVS (y :: yK) ->
  95   ( xVar meta (xVS ++ yVS) x
  96   , yVar meta (xVS ++ yVS) y
  97   )
  98 appendVars x y =
  99   ( allocVarsR (lenVar y) x
 100   , allocVarsL (lenVar x) y
 101   )
 102
 103 -- ** Type 'IndexVar'
 104
 105 -- | Index of a 'Var'.
 106 type IndexVar = Int
 107
 108 indexVar :: Var meta vs v -> Int
 109 indexVar VarZ{} = 0
 110 indexVar (VarS v) = 1 Prelude.+ indexVar v
 111
 112 -- instance KindOf (Var meta vs) where
 113 --   kindOf = fmap go
 114 --     where
 115 --     go :: forall vs2 aK a. Var meta vs2 (Proxy (a::aK)) -> TypeRep aK
 116 --     go VarZ{varKind} = varKind
 117 --     go (VarS v) = go v
 118
 119 -- * Type 'Vars'
 120 type Vars meta vs = Map.Map Name (VarV meta vs)
 121
 122 lookupVar :: Name -> Vars meta vs -> Maybe (VarV meta vs)
 123 lookupVar = Map.lookup
 124
 125 insertVar :: Name -> VarV meta vs -> Vars meta vs -> Vars meta vs
 126 insertVar = Map.insert
 127
 128 -- * Type 'UsedVars'
 129
 130 -- | List of 'Var's, used to change the context of a 'Var'
 131 -- when removing unused 'Var's.
 132 data UsedVars oldVS meta newVS a where
 133   UsedVarsZ :: UsedVars oldVS meta '[] a
 134   UsedVarsS ::
 135     Var meta oldVS (v :: vK) ->
 136     UsedVars oldVS meta newVS a ->
 137     UsedVars oldVS meta (Proxy (v :: vK) ': newVS) a
 138
 139 instance LenVar (UsedVars oldVS) where
 140   lenVar UsedVarsZ = LenZ
 141   lenVar (UsedVarsS _v oldVS) = LenS $ lenVar oldVS
 142
 143 lookupUsedVars ::
 144   Var meta oldVS (v :: vK) ->
 145   UsedVars oldVS meta newVS a ->
 146   Maybe (Var meta newVS (v :: vK))
 147 lookupUsedVars _v UsedVarsZ = Nothing
 148 lookupUsedVars v (UsedVarsS v' us) = do
 149   case v `eqTy` v' of
 150     Just HRefl ->
 151       case v' of
 152         Var{varKind, varMeta} ->
 153           Just
 154             VarZ
 155               { varZNext = lenVar us
 156               , varZKind = varKind
 157               , varZMeta = varMeta
 158               }
 159     Nothing -> VarS Data.Functor.<$> lookupUsedVars v us
 160
 161 insertUsedVars ::
 162   Var meta vs v ->
 163   UsedVars vs meta us a ->
 164   Maybe (UsedVars vs meta (Proxy v ': us) a)
 165 insertUsedVars v vs =
 166   case lookupUsedVars v vs of
 167     Just{} -> Nothing
 168     Nothing -> Just (UsedVarsS v vs)
 169
 170 -- * Class 'VarOccursIn'
 171
 172 -- | Test whether a given 'Var' occurs within @(t)@.
 173 class VarOccursIn (t :: Type -> [Type] -> aK -> Type) where
 174   varOccursIn :: Var meta vs v -> t meta vs a -> Bool
 175
 176 -- * Class 'UsedVarsOf'
 177 class UsedVarsOf t where
 178   usedVarsOf ::
 179     UsedVars vs meta oldVS a ->
 180     t meta vs b ->
 181     (forall newVS. UsedVars vs meta newVS a -> ret) ->
 182     ret
 183
 184 -- * Type 'Ty'
 185
 186 -- Use a CUSK, because it's a polymorphically recursive type,
 187 -- See https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/
 188 data Ty :: forall aK. Type -> [Type] -> aK -> Type where
 189   TyConst :: {tyConst :: Const meta a, tyConstLen :: Len vs} -> Ty meta vs a
 190   TyVar :: {tyVar :: Var meta vs a, tyVarName :: Name} -> Ty meta vs a
 191   TyApp :: {tyAppFun :: Ty meta vs f, tyAppArg :: Ty meta vs a} -> Ty meta vs (f a)
 192 infixl 9 `TyApp`
 193
 194 tyOfTypeRep :: meta -> Len vs -> TypeRep a -> Ty meta vs a
 195 tyOfTypeRep meta len ty = case ty of
 196   App f x -> TyApp{tyAppFun = tyOfTypeRep meta len f, tyAppArg = tyOfTypeRep meta len x}
 197   constType -> TyConst{tyConst = Const{constType, constMeta = meta}, tyConstLen = len}
 198
 199 -- | Monomorphic 'Ty' from a 'Typeable'.
 200 monoTy :: forall {aK} (a :: aK) meta. Typeable a => Monoid meta => Ty meta '[] a
 201 monoTy = tyOfTypeRep mempty LenZ typeRep
 202
 203 aTy :: LenInj vs => Monoid meta => Ty meta (Proxy a ': vs) (a :: Type)
 204 bTy :: LenInj vs => Monoid meta => Ty meta (Proxy a ': Proxy b ': vs) (b :: Type)
 205 cTy :: LenInj vs => Monoid meta => Ty meta (Proxy a : Proxy b : Proxy c : vs) (c :: Type)
 206 dTy :: LenInj vs => Monoid meta => Ty meta (Proxy a : Proxy b : Proxy c : Proxy d : vs) (d :: Type)
 207 aTy = TyVar{tyVar = VarZ{varZKind = monoTy @Type, varZNext = lenInj, varZMeta = mempty}, tyVarName = "a"}
 208 bTy = TyVar{tyVar = VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj, varZMeta = mempty}, tyVarName = "b"}
 209 cTy = TyVar{tyVar = VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj, varZMeta = mempty}, tyVarName = "c"}
 210 dTy = TyVar{tyVar = VarS $ VarS $ VarS $ VarZ{varZKind = monoTy @Type, varZNext = lenInj, varZMeta = mempty}, tyVarName = "d"}
 211
 212 pattern FUN ::
 213   -- CReq
 214   forall k (fun :: k) meta vs.
 215   () =>
 216   {-Monoid meta-}
 217   -- CProv
 218   forall
 219     (r1 :: RuntimeRep)
 220     (r2 :: RuntimeRep)
 221     (arg :: TYPE r1)
 222     (res :: TYPE r2).
 223   ( k ~ Type
 224   , fun ~~ (arg -> res)
 225   -- , r1 ~ LiftedRep
 226   -- , r2 ~ LiftedRep {- fixme: remove those 2 constraints -}
 227   ) =>
 228   Ty meta vs arg ->
 229   Ty meta vs res ->
 230   Ty meta vs fun
 231 pattern FUN arg res <-
 232   TyApp
 233     { tyAppFun =
 234       TyApp
 235         { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
 236         , tyAppArg = arg
 237         }
 238     , tyAppArg = res
 239     }
 240
 241 (~>) :: Monoid meta => Ty meta vs a -> Ty meta vs b -> Ty meta vs (a -> b)
 242 (~>) arg res =
 243   TyApp
 244     { tyAppFun =
 245         TyApp
 246           { tyAppFun =
 247               TyConst{tyConst = Const{constType = typeRep, constMeta = mempty}, tyConstLen = (lenVar arg)}
 248           , tyAppArg = arg
 249           }
 250     , tyAppArg = res
 251     }
 252 infixr 0 ~>
 253
 254 deriving instance Show meta => Show (Ty meta vs a)
 255
 256 -- type instance SourceOf (Ty vs src t) = src
 257 instance LenVar Ty where
 258   lenVar TyConst{tyConstLen} = tyConstLen
 259   lenVar TyApp{tyAppFun} = lenVar tyAppFun
 260   lenVar TyVar{tyVar} = lenVar tyVar
 261
 262 -- lenVars (TyFam l _f _as) = l
 263 instance AllocVars Ty where
 264   allocVarsL len ty@TyConst{..} = ty{tyConstLen = addLen len tyConstLen}
 265   allocVarsL len TyApp{..} = TyApp{tyAppFun = allocVarsL len tyAppFun, tyAppArg = allocVarsL len tyAppArg}
 266   allocVarsL len ty@TyVar{..} = ty{tyVar = allocVarsL len tyVar}
 267
 268   -- allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as
 269
 270   allocVarsR len ty@TyConst{..} = ty{tyConstLen = addLen tyConstLen len}
 271   allocVarsR len TyApp{..} = TyApp{tyAppFun = allocVarsR len tyAppFun, tyAppArg = allocVarsR len tyAppArg, ..}
 272   allocVarsR len ty@TyVar{..} = ty{tyVar = allocVarsR len tyVar}
 273
 274 -- allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as
 275 instance VarOccursIn Ty where
 276   varOccursIn v TyVar{tyVar = v'} | Just{} <- v `eqTy` v' = False
 277   varOccursIn _v TyVar{} = False
 278   varOccursIn _v TyConst{} = False
 279   varOccursIn v TyApp{tyAppFun = f, tyAppArg = a} = varOccursIn v f Prelude.|| varOccursIn v a
 280
 281 -- varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as
 282 instance UsedVarsOf Ty where
 283   usedVarsOf vs TyConst{} k = k vs
 284   usedVarsOf vs TyApp{tyAppFun = f, tyAppArg = a} k =
 285     usedVarsOf vs f $ \vs' ->
 286       usedVarsOf vs' a k
 287   usedVarsOf vs TyVar{tyVar = v} k =
 288     case insertUsedVars v vs of
 289       Nothing -> k vs
 290       Just vs' -> k vs'
 291
 292 -- usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k
 293
 294 -- ** Type 'TyT'
 295
 296 -- | Existential for 'Type'.
 297 data TyT meta vs = forall a. TyT (Ty meta vs a)
 298
 299 -- type instance SourceOf (TyT vs src) = src
 300 instance Eq (TyT meta vs) where
 301   TyT x == TyT y = isJust $ eqTy x y
 302 instance Show meta => Show (TyT meta vs) where
 303   showsPrec p (TyT x) = showsPrec p x
 304
 305 -- * Type 'Kind'
 306 type Kind meta a = Ty meta '[] a
 307
 308 -- ** Type 'KindK'
 309 type KindK meta = TyT meta '[]
 310
 311 -- ** Type 'TyVT'
 312 data TyVT meta = forall vs a. TyVT (Ty meta vs a)
 313
 314 deriving instance Show meta => Show (TyVT meta)
 315 instance Eq (TyVT m) where
 316   TyVT x == TyVT y = isJust (eqTy x' y')
 317     where
 318       (x', y') = appendVars x y
 319
 320 -- instance (Monoid src) => EqTy (MT.Writer src) (MT.Writer src) where
 321 --  eqTy x y = eqTy (unSourced x) (unSourced y)
 322 instance EqTy (Ty meta vs) (Ty meta vs) where
 323   eqTy = go
 324     where
 325       go :: forall xK xT yK yT. Ty meta vs (xT :: xK) -> Ty meta vs (yT :: yK) -> Maybe (xT :~~: yT)
 326       go TyConst{tyConst = x} TyConst{tyConst = y} = eqTy x y
 327       go TyVar{tyVar = x} TyVar{tyVar = y} = eqTy x y
 328       go TyApp{tyAppFun = xF, tyAppArg = xA} TyApp{tyAppFun = yF, tyAppArg = yA}
 329         | Just HRefl <- go xF yF
 330         , Just HRefl <- go xA yA =
 331             Just HRefl
 332       go _x _y = Nothing
 333
 334 -- eqTy (TyFam _ _lx xF xA) (TyFam _ _ly yF yA)
 335 --  | Just HRefl <- eqTypeRep xF yF
 336 --  , Just HRefl <- eqTys xA yA
 337 --  = Just HRefl
 338 -- -- NOTE: 'TyFam' is expanded as much as possible.
 339 -- eqTy x@TyFam{} y = eqTy (expandFam x) y
 340 -- eqTy x y@TyFam{} = eqTy x (expandFam y)
 341
 342 -- * Type 'Tys'
 343 data Tys (as :: [Type]) meta vs (a :: aK) where
 344   TysZ :: Tys '[] meta vs a
 345   TysS :: Ty meta vs a -> Tys as meta vs b -> Tys (Proxy a ': as) meta vs b
 346 infixr 5 `TysS`
 347
 348 -- type instance SourceOf (Tys vs src ts) = src
 349 -- instance ConstsOf (Tys meta vs ts) where
 350 --  constsOf TysZ = Set.empty
 351 --  constsOf (TysS t ts) = constsOf t `Set.union` constsOf ts
 352 instance UsedVarsOf (Tys as) where
 353   usedVarsOf vs TysZ k = k vs
 354   usedVarsOf vs (TysS t ts) k =
 355     usedVarsOf vs t $ \vs' ->
 356       usedVarsOf vs' ts k
 357 instance VarOccursIn (Tys as) where
 358   varOccursIn _v TysZ = False
 359   varOccursIn v (TysS t ts) = varOccursIn v t Prelude.|| varOccursIn v ts
 360
 361 -- ** Type family 'FunArg'
 362 type family FunArg (fun :: Type) :: Type where
 363   FunArg (q #> f) = FunArg f
 364   FunArg (a -> b) = a
 365
 366 -- ** Type family 'FunRes'
 367 type family FunRes (fun :: Type) :: Type where
 368   FunRes (q #> f) = FunRes f
 369   FunRes (a -> b) = b
 370
 371 -- -- | Return, when the given 'Type' is a function,
 372 -- -- the argument of that function.
 373 -- unTyFun ::
 374 --  forall t src tys.
 375 --  SourceInj (TyVT src) src =>
 376 --  --Constable (->) =>
 377 --  Type src tys t ->
 378 --  Maybe ( Type src tys (FunArg t)
 379 --        , Type src tys (FunRes t) )
 380 -- unTyFun ty_ini = go ty_ini
 381 --   where
 382 --   go ::
 383 --    Type src tys x ->
 384 --    Maybe ( Type src tys (FunArg x)
 385 --          , Type src tys (FunRes x) )
 386 --   go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
 387 --    | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
 388 --    = Just ((a `withSource` TyVT ty_ini), (b `withSource` TyVT ty_ini))
 389 --   go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
 390 --    | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
 391 --    = go b
 392 --   go TyApp{}   = Nothing
 393 --   go TyConst{} = Nothing
 394 --   go TyVar{}   = Nothing
 395 --   go TyFam{}   = Nothing
 396
 397 proj_ConstKi ::
 398   forall kc (c :: kc) u meta.
 399   Typeable c =>
 400   -- (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 401   -- KindInjP (Ty_of_Type kc) =>
 402   Const meta u ->
 403   Maybe (c :~~: u)
 404 proj_ConstKi = eqTypeRep (typeRep @c) . constType
 405
 406 -- ** Type @(#>)@
 407
 408 -- | /Type constant/ to qualify a 'Type'.
 409 newtype (#>) (q :: Constraint) (a :: Type) = Qual (q => a)
 410
 411 -- | Qualify a 'Type'.
 412 (#>) :: Monoid meta => Ty meta vs q -> Ty meta vs t -> Ty meta vs (q #> t)
 413 (#>) q t =
 414   -- (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
 415   TyApp
 416     { tyAppFun =
 417         TyApp
 418           { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#>), constMeta = mempty}, tyConstLen = lenVar q}
 419           , tyAppArg = q
 420           }
 421     , tyAppArg = t
 422     }
 423
 424 infixr 0 #>
 425
 426 -- NOTE: should actually be (-1)
 427 -- to compose well with @infixr 0 (->)@
 428 -- but this is not allowed by GHC.
 429
 430 -- ** Class @(#)@
 431
 432 -- | 'Constraint' union.
 433 class ((x, y) :: Constraint) => x # y
 434
 435 instance ((x, y) :: Constraint) => x # y
 436
 437 -- | Unify two 'K.Constraint's.
 438 (#) :: Monoid meta => Ty meta vs qx -> Ty meta vs qy -> Ty meta vs (qx # qy)
 439 (#) a b =
 440   -- (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
 441   TyApp
 442     { tyAppFun =
 443         TyApp
 444           { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#), constMeta = mempty}, tyConstLen = lenVar a}
 445           , tyAppArg = a
 446           }
 447     , tyAppArg = b
 448     }
 449
 450 infixr 2 #
 451
 452 -- * Class 'KindOf'
 453 class KindOf (ty :: Type -> [Type] -> aK -> Type) where
 454   -- | Return the kind of the given 'Var'.
 455   kindOf ::
 456     -- HasCallStack =>
 457     Show meta =>
 458     ty meta vs (a :: aK) ->
 459     Kind meta (aK :: Type)
 460
 461 instance KindOf Var where
 462   kindOf Var{varKind} = varKind
 463 instance KindOf Ty where
 464   kindOf TyConst{tyConst = Const{..} :: Const meta (a :: aK)} =
 465     tyOfTypeRep constMeta LenZ (typeRepKind constType)
 466   kindOf TyApp{tyAppFun = f} = case kindOf f of
 467     TyApp
 468       { tyAppFun =
 469         TyApp
 470           { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
 471           }
 472       , tyAppArg = k
 473       } -> k
 474     t -> error $ "here: " <> show t
 475   kindOf TyVar{tyVar = Var{varKind, varMeta}} = varKind
 476
 477 -- kindOf (TyFam _src _len fam _as) = kindOfConst fam