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