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