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