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, withTypeable, (:~~:) (..))
  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   tyOf :: meta -> Len vs -> Ty meta vs a
 213 instance (Tyable a, Tyable b) => Tyable (a b) where
 214   tyOf meta vs = TyApp (tyOf @a meta vs) (tyOf @b meta vs)
 215 instance {-# OVERLAPPABLE #-} Typeable a => Tyable a where
 216   tyOf meta vs = TyConst{tyConst = Const{constType = typeRep, constMeta = meta}, tyConstLen = vs}
 217
 218 typeOf :: Monoid meta => Tyable a => Ty meta '[] a
 219 typeOf = tyOf mempty LenZ
 220
 221 pattern FUN ::
 222   -- CReq
 223   forall k (fun :: k) meta vs.
 224   () =>
 225   {-Monoid meta-}
 226   -- CProv
 227   forall
 228     (r1 :: RuntimeRep)
 229     (r2 :: RuntimeRep)
 230     (arg :: TYPE r1)
 231     (res :: TYPE r2).
 232   ( k ~ Type
 233   , fun ~~ (arg -> res)
 234   -- , r1 ~ LiftedRep
 235   -- , r2 ~ LiftedRep {- fixme: remove those 2 constraints -}
 236   ) =>
 237   Ty meta vs arg ->
 238   Ty meta vs res ->
 239   Ty meta vs fun
 240 pattern FUN arg res <-
 241   TyApp
 242     { tyAppFun =
 243       TyApp
 244         { tyAppFun = TyConst{tyConst = Const{constType = eqTypeRep (typeRep @(->)) -> Just HRefl}}
 245         , tyAppArg = arg
 246         }
 247     , tyAppArg = res
 248     }
 249
 250 (~>) :: Monoid meta => Ty meta vs a -> Ty meta vs b -> Ty meta vs (a -> b)
 251 (~>) arg res =
 252   TyApp
 253     { tyAppFun =
 254         TyApp
 255           { tyAppFun = tyOf @(->) mempty (lenVar arg)
 256           , tyAppArg = arg
 257           }
 258     , tyAppArg = res
 259     }
 260 infixr 0 ~>
 261
 262 deriving instance Show meta => Show (Ty meta vs a)
 263
 264 -- type instance SourceOf (Ty vs src t) = src
 265 instance LenVar Ty where
 266   lenVar TyConst{tyConstLen} = tyConstLen
 267   lenVar TyApp{tyAppFun} = lenVar tyAppFun
 268   lenVar TyVar{tyVar} = lenVar tyVar
 269
 270 -- lenVars (TyFam l _f _as) = l
 271 instance AllocVars Ty where
 272   allocVarsL len ty@TyConst{..} = ty{tyConstLen = addLen len tyConstLen}
 273   allocVarsL len TyApp{..} = TyApp{tyAppFun = allocVarsL len tyAppFun, tyAppArg = allocVarsL len tyAppArg}
 274   allocVarsL len ty@TyVar{..} = ty{tyVar = allocVarsL len tyVar}
 275
 276   -- allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as
 277
 278   allocVarsR len ty@TyConst{..} = ty{tyConstLen = addLen tyConstLen len}
 279   allocVarsR len TyApp{..} = TyApp{tyAppFun = allocVarsR len tyAppFun, tyAppArg = allocVarsR len tyAppArg, ..}
 280   allocVarsR len ty@TyVar{..} = ty{tyVar = allocVarsR len tyVar}
 281
 282 -- allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as
 283 instance VarOccursIn Ty where
 284   varOccursIn v TyVar{tyVar = v'} | Just{} <- v `eqTy` v' = False
 285   varOccursIn _v TyVar{} = False
 286   varOccursIn _v TyConst{} = False
 287   varOccursIn v TyApp{tyAppFun = f, tyAppArg = a} = varOccursIn v f Prelude.|| varOccursIn v a
 288
 289 -- varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as
 290 instance UsedVarsOf Ty where
 291   usedVarsOf vs TyConst{} k = k vs
 292   usedVarsOf vs TyApp{tyAppFun = f, tyAppArg = a} k =
 293     usedVarsOf vs f $ \vs' ->
 294       usedVarsOf vs' a k
 295   usedVarsOf vs TyVar{tyVar = v} k =
 296     case insertUsedVars v vs of
 297       Nothing -> k vs
 298       Just vs' -> k vs'
 299
 300 -- usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k
 301
 302 -- ** Type 'TyT'
 303
 304 -- | Existential for 'Type'.
 305 data TyT meta vs = forall a. TyT (Ty meta vs a)
 306
 307 -- type instance SourceOf (TyT vs src) = src
 308 instance Eq (TyT meta vs) where
 309   TyT x == TyT y = isJust $ eqTy x y
 310 instance Show meta => Show (TyT meta vs) where
 311   showsPrec p (TyT x) = showsPrec p x
 312
 313 -- * Type 'Kind'
 314 type Kind meta a = Ty meta '[] a
 315
 316 -- ** Type 'KindK'
 317 type KindK meta = TyT meta '[]
 318
 319 -- ** Type 'TyVT'
 320 data TyVT meta = forall vs a. TyVT (Ty meta vs a)
 321
 322 deriving instance Show meta => Show (TyVT meta)
 323 instance Eq (TyVT m) where
 324   TyVT x == TyVT y = isJust (eqTy x' y')
 325     where
 326       (x', y') = appendVars x y
 327
 328 -- instance (Monoid src) => EqTy (MT.Writer src) (MT.Writer src) where
 329 --  eqTy x y = eqTy (unSourced x) (unSourced y)
 330 instance EqTy (Ty meta vs) (Ty meta vs) where
 331   eqTy TyConst{tyConst = x} TyConst{tyConst = y} = eqTy x y
 332   eqTy TyVar{tyVar = x} TyVar{tyVar = y} = eqTy x y
 333   eqTy TyApp{tyAppFun = xF, tyAppArg = xA} TyApp{tyAppFun = yF, tyAppArg = yA}
 334     | Just HRefl <- eqTy xF yF
 335     , Just HRefl <- eqTy xA yA =
 336         Just HRefl
 337   eqTy _x _y = Nothing
 338
 339 -- eqTy (TyFam _ _lx xF xA) (TyFam _ _ly yF yA)
 340 --  | Just HRefl <- eqTypeRep xF yF
 341 --  , Just HRefl <- eqTys xA yA
 342 --  = Just HRefl
 343 -- -- NOTE: 'TyFam' is expanded as much as possible.
 344 -- eqTy x@TyFam{} y = eqTy (expandFam x) y
 345 -- eqTy x y@TyFam{} = eqTy x (expandFam y)
 346
 347 -- * Type 'Tys'
 348 data Tys (as :: [Type]) meta vs (a :: aK) where
 349   TysZ :: Tys '[] meta vs a
 350   TysS :: Ty meta vs a -> Tys as meta vs b -> Tys (Proxy a ': as) meta vs b
 351 infixr 5 `TysS`
 352
 353 -- type instance SourceOf (Tys vs src ts) = src
 354 -- instance ConstsOf (Tys meta vs ts) where
 355 --  constsOf TysZ = Set.empty
 356 --  constsOf (TysS t ts) = constsOf t `Set.union` constsOf ts
 357 instance UsedVarsOf (Tys as) where
 358   usedVarsOf vs TysZ k = k vs
 359   usedVarsOf vs (TysS t ts) k =
 360     usedVarsOf vs t $ \vs' ->
 361       usedVarsOf vs' ts k
 362 instance VarOccursIn (Tys as) where
 363   varOccursIn _v TysZ = False
 364   varOccursIn v (TysS t ts) = varOccursIn v t Prelude.|| varOccursIn v ts
 365
 366 -- ** Type family 'FunArg'
 367 type family FunArg (fun :: Type) :: Type where
 368   FunArg (q #> f) = FunArg f
 369   FunArg (a -> b) = a
 370
 371 -- ** Type family 'FunRes'
 372 type family FunRes (fun :: Type) :: Type where
 373   FunRes (q #> f) = FunRes f
 374   FunRes (a -> b) = b
 375
 376 -- -- | Return, when the given 'Type' is a function,
 377 -- -- the argument of that function.
 378 -- unTyFun ::
 379 --  forall t src tys.
 380 --  SourceInj (TyVT src) src =>
 381 --  --Constable (->) =>
 382 --  Type src tys t ->
 383 --  Maybe ( Type src tys (FunArg t)
 384 --        , Type src tys (FunRes t) )
 385 -- unTyFun ty_ini = go ty_ini
 386 --   where
 387 --   go ::
 388 --    Type src tys x ->
 389 --    Maybe ( Type src tys (FunArg x)
 390 --          , Type src tys (FunRes x) )
 391 --   go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
 392 --    | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
 393 --    = Just ((a `withSource` TyVT ty_ini), (b `withSource` TyVT ty_ini))
 394 --   go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
 395 --    | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
 396 --    = go b
 397 --   go TyApp{}   = Nothing
 398 --   go TyConst{} = Nothing
 399 --   go TyVar{}   = Nothing
 400 --   go TyFam{}   = Nothing
 401
 402 proj_ConstKi ::
 403   forall kc (c :: kc) u meta.
 404   Typeable c =>
 405   -- (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 406   -- KindInjP (Ty_of_Type kc) =>
 407   Const meta u ->
 408   Maybe (c :~~: u)
 409 proj_ConstKi = eqTypeRep (typeRep @c) . constType
 410
 411 -- HRefl <- eqTy ku kc -- $ kindInjP @(Ty_of_Type kc) ()
 412 -- HRefl :: u:~~:c <- eqT
 413 -- Just HRefl
 414
 415 -- ** Type @(#>)@
 416
 417 -- | /Type constant/ to qualify a 'Type'.
 418 newtype (#>) (q :: Constraint) (a :: Type) = Qual (q => a)
 419
 420 -- | Qualify a 'Type'.
 421 (#>) :: Monoid meta => Ty meta vs q -> Ty meta vs t -> Ty meta vs (q #> t)
 422 (#>) q t =
 423   -- (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
 424   TyApp
 425     { tyAppFun =
 426         TyApp
 427           { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#>), constMeta = mempty}, tyConstLen = lenVar q}
 428           , tyAppArg = q
 429           }
 430     , tyAppArg = t
 431     }
 432
 433 infixr 0 #>
 434
 435 -- NOTE: should actually be (-1)
 436 -- to compose well with @infixr 0 (->)@
 437 -- but this is not allowed by GHC.
 438
 439 -- ** Class @(#)@
 440
 441 -- | 'Constraint' union.
 442 class ((x, y) :: Constraint) => x # y
 443
 444 instance ((x, y) :: Constraint) => x # y
 445
 446 -- | Unify two 'K.Constraint's.
 447 (#) :: Monoid meta => Ty meta vs qx -> Ty meta vs qy -> Ty meta vs (qx # qy)
 448 (#) a b =
 449   -- (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
 450   TyApp
 451     { tyAppFun =
 452         TyApp
 453           { tyAppFun = TyConst{tyConst = Const{constType = typeRep @(#), constMeta = mempty}, tyConstLen = lenVar a}
 454           , tyAppArg = a
 455           }
 456     , tyAppArg = b
 457     }
 458
 459 infixr 2 #
 460
 461 -- * Class 'KindOf'
 462 class KindOf (ty :: Type -> [Type] -> aK -> Type) where
 463   -- | Return the kind of the given 'Var'.
 464   kindOf ::
 465     -- Provenanceable (ProvenanceKindOf t) m =>
 466     -- MC.MonadWriter (ProvenanceKindOf t) m =>
 467     Show meta =>
 468     ty meta vs (a :: aK) ->
 469     Kind meta aK
 470
 471 instance KindOf Var where
 472   kindOf Var{varKind} = varKind
 473 instance KindOf Ty where
 474   kindOf TyConst{tyConst = Const{constType, constMeta} :: Const meta (a :: aK)} =
 475     withTypeable (typeRepKind constType) $
 476       tyOf @aK constMeta LenZ
 477   kindOf TyApp{tyAppFun = f} = case kindOf f of
 478     FUN _ kf -> kf
 479     t -> error $ "here: " <> show t
 480   kindOf TyVar{tyVar = Var{varKind, varMeta}} = varKind
 481
 482 -- kindOf (TyFam _src _len fam _as) = kindOfConst fam