src/Symantic/Typer/Type.hs

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