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, typeRepKind, (:~~:) (..), pattern App)
  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) =
  36   -- InferTyable aK =>
  37   Const
  38   { constType :: TypeRep a
  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 tyOfTypeRep :: meta -> Len vs -> TypeRep a -> Ty meta vs a
 201 tyOfTypeRep meta len ty = case ty of
 202   App f x -> TyApp{tyAppFun = tyOfTypeRep meta len f, tyAppArg = tyOfTypeRep meta len x}
 203   constType -> TyConst{tyConst = Const{constType, constMeta = meta}, tyConstLen = len}
 204
 205 -- | Monomorphic 'Ty' from a 'Typeable'.
 206 monoTy :: forall {aK} (a :: aK) meta. Typeable a => Monoid meta => Ty meta '[] a
 207 monoTy = tyOfTypeRep mempty LenZ typeRep
 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 (~>) :: Monoid meta => Ty meta vs a -> Ty meta vs b -> Ty meta vs (a -> b)
 239 (~>) arg res =
 240   TyApp
 241     { tyAppFun =
 242         TyApp
 243           { tyAppFun =
 244               TyConst{tyConst = Const{constType = typeRep, constMeta = mempty}, tyConstLen = (lenVar arg)}
 245           , tyAppArg = arg
 246           }
 247     , tyAppArg = res
 248     }
 249 infixr 0 ~>
 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 = go
 321     where
 322       go :: forall xK xT yK yT. Ty meta vs (xT :: xK) -> Ty meta vs (yT :: yK) -> Maybe (xT :~~: yT)
 323       go TyConst{tyConst = x} TyConst{tyConst = y} = eqTy x y
 324       go TyVar{tyVar = x} TyVar{tyVar = y} = eqTy x y
 325       go TyApp{tyAppFun = xF, tyAppArg = xA} TyApp{tyAppFun = yF, tyAppArg = yA}
 326         | Just HRefl <- go xF yF
 327         , Just HRefl <- go xA yA =
 328             Just HRefl
 329       go _x _y = Nothing
 330
 331 -- eqTy (TyFam _ _lx xF xA) (TyFam _ _ly yF yA)
 332 --  | Just HRefl <- eqTypeRep xF yF
 333 --  , Just HRefl <- eqTys xA yA
 334 --  = Just HRefl
 335 -- -- NOTE: 'TyFam' is expanded as much as possible.
 336 -- eqTy x@TyFam{} y = eqTy (expandFam x) y
 337 -- eqTy x y@TyFam{} = eqTy x (expandFam y)
 338
 339 -- * Type 'Tys'
 340 data Tys (as :: [Type]) meta vs (a :: aK) where
 341   TysZ :: Tys '[] meta vs a
 342   TysS :: Ty meta vs a -> Tys as meta vs b -> Tys (Proxy a ': as) meta vs b
 343 infixr 5 `TysS`
 344
 345 -- type instance SourceOf (Tys vs src ts) = src
 346 -- instance ConstsOf (Tys meta vs ts) where
 347 --  constsOf TysZ = Set.empty
 348 --  constsOf (TysS t ts) = constsOf t `Set.union` constsOf ts
 349 instance UsedVarsOf (Tys as) where
 350   usedVarsOf vs TysZ k = k vs
 351   usedVarsOf vs (TysS t ts) k =
 352     usedVarsOf vs t $ \vs' ->
 353       usedVarsOf vs' ts k
 354 instance VarOccursIn (Tys as) where
 355   varOccursIn _v TysZ = False
 356   varOccursIn v (TysS t ts) = varOccursIn v t Prelude.|| varOccursIn v ts
 357
 358 -- ** Type family 'FunArg'
 359 type family FunArg (fun :: Type) :: Type where
 360   FunArg (q #> f) = FunArg f
 361   FunArg (a -> b) = a
 362
 363 -- ** Type family 'FunRes'
 364 type family FunRes (fun :: Type) :: Type where
 365   FunRes (q #> f) = FunRes f
 366   FunRes (a -> b) = b
 367
 368 -- -- | Return, when the given 'Type' is a function,
 369 -- -- the argument of that function.
 370 -- unTyFun ::
 371 --  forall t src tys.
 372 --  SourceInj (TyVT src) src =>
 373 --  --Constable (->) =>
 374 --  Type src tys t ->
 375 --  Maybe ( Type src tys (FunArg t)
 376 --        , Type src tys (FunRes t) )
 377 -- unTyFun ty_ini = go ty_ini
 378 --   where
 379 --   go ::
 380 --    Type src tys x ->
 381 --    Maybe ( Type src tys (FunArg x)
 382 --          , Type src tys (FunRes x) )
 383 --   go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
 384 --    | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
 385 --    = Just ((a `withSource` TyVT ty_ini), (b `withSource` TyVT ty_ini))
 386 --   go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
 387 --    | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
 388 --    = go b
 389 --   go TyApp{}   = Nothing
 390 --   go TyConst{} = Nothing
 391 --   go TyVar{}   = Nothing
 392 --   go TyFam{}   = Nothing
 393
 394 proj_ConstKi ::
 395   forall kc (c :: kc) u meta.
 396   Typeable c =>
 397   -- (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 398   -- KindInjP (Ty_of_Type kc) =>
 399   Const meta u ->
 400   Maybe (c :~~: u)
 401 proj_ConstKi = eqTypeRep (typeRep @c) . constType
 402
 403 -- ** Type @(#>)@
 404
 405 -- | /Type constant/ to qualify a 'Type'.
 406 newtype (#>) (q :: Constraint) (a :: Type) = Qual (q => a)
 407
 408 -- | Qualify a 'Type'.
 409 (#>) :: Monoid meta => Ty meta vs q -> Ty meta vs t -> Ty meta vs (q #> t)
 410 (#>) q t =
 411   -- (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
 412   TyApp
 413     { tyAppFun =
 414         TyApp
 415           { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#>), constMeta = mempty}, tyConstLen = lenVar q}
 416           , tyAppArg = q
 417           }
 418     , tyAppArg = t
 419     }
 420
 421 infixr 0 #>
 422
 423 -- NOTE: should actually be (-1)
 424 -- to compose well with @infixr 0 (->)@
 425 -- but this is not allowed by GHC.
 426
 427 -- ** Class @(#)@
 428
 429 -- | 'Constraint' union.
 430 class ((x, y) :: Constraint) => x # y
 431
 432 instance ((x, y) :: Constraint) => x # y
 433
 434 -- | Unify two 'K.Constraint's.
 435 (#) :: Monoid meta => Ty meta vs qx -> Ty meta vs qy -> Ty meta vs (qx # qy)
 436 (#) a b =
 437   -- (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
 438   TyApp
 439     { tyAppFun =
 440         TyApp
 441           { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#), constMeta = mempty}, tyConstLen = lenVar a}
 442           , tyAppArg = a
 443           }
 444     , tyAppArg = b
 445     }
 446
 447 infixr 2 #
 448
 449 -- * Class 'KindOf'
 450 class KindOf (ty :: Type -> [Type] -> aK -> Type) where
 451   -- | Return the kind of the given 'Var'.
 452   kindOf ::
 453     -- HasCallStack =>
 454     Show meta =>
 455     ty meta vs (a :: aK) ->
 456     Kind meta (aK :: Type)
 457
 458 instance KindOf Var where
 459   kindOf Var{varKind} = varKind
 460 instance KindOf Ty where
 461   kindOf TyConst{tyConst = Const{..} :: Const meta (a :: aK)} =
 462     tyOfTypeRep constMeta LenZ (typeRepKind constType)
 463   kindOf TyApp{tyAppFun = f} = case kindOf f of
 464     TyApp
 465       { tyAppFun =
 466         TyApp
 467           { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
 468           }
 469       , tyAppArg = k
 470       } -> k
 471     t -> error $ "here: " <> show t
 472   kindOf TyVar{tyVar = Var{varKind, varMeta}} = varKind
 473
 474 -- kindOf (TyFam _src _len fam _as) = kindOfConst fam