symantic/Language/Symantic/Typing/Type.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE TypeInType #-}
   5 {-# LANGUAGE UndecidableInstances #-}
   6 {-# LANGUAGE UndecidableSuperClasses #-}
   7 {-# language ConstraintKinds #-}
   8 {-# OPTIONS_GHC -fno-warn-orphans #-}
   9 module Language.Symantic.Typing.Type
  10  ( module Language.Symantic.Typing.Type
  11  , Proxy(..)
  12  , (:~:)(..)
  13  , (:~~:)(..)
  14  , K.Constraint
  15  ) where
  16
  17 import Control.Applicative (Alternative(..))
  18 import Data.Maybe (isJust)
  19 import Data.Proxy
  20 import Data.Semigroup ((<>))
  21 import Data.Set (Set)
  22 import Data.Type.Equality
  23 import Data.Typeable
  24 import qualified Data.Kind as K
  25 import qualified Data.Set as Set
  26
  27 import Language.Symantic.Grammar
  28 import Language.Symantic.Typing.List
  29 import Language.Symantic.Typing.Kind
  30 import Language.Symantic.Typing.Variable
  31 import Language.Symantic.Typing.Module
  32
  33 -- * Type 'Type'
  34 data Type (src::K.Type) (vs::[K.Type]) (t::kt) where
  35         TyConst :: src -> Len vs
  36                        -> Const src c
  37                        -> Type src vs c
  38         TyApp   :: src -> Type src vs f
  39                        -> Type src vs a
  40                        -> Type src vs (f a)
  41                        -- NOTE: @f a@ decomposition made possible
  42                        -- at the cost of requiring @TypeInType@.
  43         TyVar   :: src -> NameVar
  44                        -> Var src vs v
  45                        -> Type src vs v
  46         TyFam   :: src -> Len vs
  47                        -> Const src fam
  48                        -> Types src vs hs
  49                        -> Type src vs (Fam fam hs)
  50         {-
  51         TyPi    :: src -> Type src (arg ': vs) res
  52                        -> Type (Pi arg res) src vs
  53         TyQuant :: src -> NameHint
  54                        -> Kind src kv
  55                        -> (forall (v::kv). Type src vs v -> TypeK src vs k)
  56                        -> Type src vs (h::k)
  57         TyEq :: src -> Type x src vs
  58                     -> Type y src vs
  59                     -> Type (x #~ y) src vs
  60         -}
  61
  62 instance Source src => Eq (Type src vs t) where
  63         x == y = isJust $ eqType x y
  64 instance SourceInj (TypeVT src) src => TestEquality (Type src vs) where
  65         testEquality = eqType
  66
  67 type instance SourceOf (Type src vs t) = src
  68 instance Source src => Sourced (Type src vs t) where
  69         sourceOf (TyConst src _l _c)     = src
  70         sourceOf (TyApp   src _f _a)     = src
  71         sourceOf (TyVar   src _n _v)     = src
  72         sourceOf (TyFam   src _l _f _as) = src
  73
  74         setSource (TyConst _src l c)    src = TyConst src l c
  75         setSource (TyApp   _src f a)    src = TyApp   src f a
  76         setSource (TyVar   _src n v)    src = TyVar   src n v
  77         setSource (TyFam   _src l f as) src = TyFam   src l f as
  78
  79 instance SourceInj (TypeVT src) src => KindOf (Type src vs) where
  80         kindOf t = kindOfType t `withSource` TypeVT t
  81
  82 instance ConstsOf (Type src vs t) where
  83         constsOf (TyConst _src _len c)    = Set.singleton $ ConstC c
  84         constsOf TyVar{}                  = Set.empty
  85         constsOf (TyApp _src f a)         = constsOf f `Set.union` constsOf a
  86         constsOf (TyFam _src _len fam as) = constsOf fam `Set.union` constsOf as
  87
  88 type instance VarsOf (Type src vs t) = vs
  89 instance LenVars (Type src vs t) where
  90         lenVars (TyConst _src len _c) = len
  91         lenVars (TyApp _src f _a)     = lenVars f
  92         lenVars (TyVar   _src _n v)   = lenVars v
  93         lenVars (TyFam _src l _f _as) = l
  94 instance UsedVarsOf (Type src vs t) where
  95         usedVarsOf vs TyConst{} k = k vs
  96         usedVarsOf vs (TyFam _src _len _fam as) k = usedVarsOf vs as k
  97         usedVarsOf vs (TyApp _src f a) k =
  98                 usedVarsOf vs f $ \vs' ->
  99                 usedVarsOf vs' a k
 100         usedVarsOf vs (TyVar _src _n v) k =
 101                 case insertUsedVars v vs of
 102                  Nothing  -> k vs
 103                  Just vs' -> k vs'
 104 instance VarOccursIn (Type src vs t) where
 105         varOccursIn v (TyVar _src _n v') | Just{} <- v `eqVarKi` v' = False
 106         varOccursIn _v TyVar{}                  = False
 107         varOccursIn _v TyConst{}                = False
 108         varOccursIn v (TyApp _src f a)          = varOccursIn v f || varOccursIn v a
 109         varOccursIn v (TyFam _src _len _fam as) = varOccursIn v as
 110 instance AllocVars (Type src) where
 111         allocVarsL len (TyConst src l c)  = TyConst src (addLen len l) c
 112         allocVarsL len (TyApp src f a)    = TyApp src (allocVarsL len f) (allocVarsL len a)
 113         allocVarsL len (TyVar src n v)    = TyVar src n $ allocVarsL len v
 114         allocVarsL len (TyFam src l f as) = TyFam src (addLen len l) f $ allocVarsL len `mapTys` as
 115
 116         allocVarsR len (TyConst src l c)  = TyConst src (addLen l len) c
 117         allocVarsR len (TyApp src f a)    = TyApp src (allocVarsR len f) (allocVarsR len a)
 118         allocVarsR len (TyVar src n v)    = TyVar src n $ allocVarsR len v
 119         allocVarsR len (TyFam src l f as) = TyFam src (addLen l len) f $ allocVarsR len `mapTys` as
 120
 121 -- | Like 'TyConst', but using 'noSource', 'lenInj' and 'constInj'.
 122 --
 123 -- FIXME: remove @kc@ when GHC's #12933 is fixed.
 124 tyConst ::
 125  forall kc (c::kc) src vs.
 126  Source src =>
 127  LenInj vs =>
 128  Constable c =>
 129  KindInjP (Ty_of_Type kc) =>
 130  Type_of_Ty (Ty_of_Type kc) ~ kc =>
 131  Type src vs c
 132 tyConst = TyConst noSource lenInj constInj
 133  -- NOTE: The forall brings @c@ first in the type variables,
 134  -- which is convenient to use @TypeApplications@.
 135
 136 -- | Like 'tyConst', but not using 'lenInj'.
 137 tyConstLen ::
 138  forall kc (c::kc) src vs.
 139  Source src =>
 140  Constable c =>
 141  KindInjP (Ty_of_Type kc) =>
 142  Type_of_Ty (Ty_of_Type kc) ~ kc =>
 143  Len vs ->
 144  Type src vs c
 145 tyConstLen len = TyConst noSource len constInj
 146
 147 -- | Like 'TyApp', but using 'noSource'.
 148 tyApp ::
 149  Source src =>
 150  Type src vs f ->
 151  Type src vs a ->
 152  Type src vs (f a)
 153 tyApp = TyApp noSource
 154 infixl 9 `tyApp`
 155
 156 -- | Like 'TyVar', but using 'noSource'.
 157 tyVar ::
 158  Source src =>
 159  NameVar ->
 160  Var src vs v ->
 161  Type src vs v
 162 tyVar = TyVar noSource
 163
 164 -- | Like 'TyFam', but using 'noSource'.
 165 --
 166 -- FIXME: remove @kc@ when GHC's #12933 is fixed.
 167 tyFam ::
 168  forall kc (c::kc) as vs src.
 169  Source src =>
 170  LenInj vs =>
 171  Constable c =>
 172  KindInjP (Ty_of_Type kc) =>
 173  Type_of_Ty (Ty_of_Type kc) ~ kc =>
 174  Types src vs as ->
 175  Type src vs (Fam c as)
 176 tyFam = TyFam noSource lenInj (constInj @c)
 177
 178 -- | Qualify a 'Type'.
 179 tyQual ::
 180  Source src =>
 181  Type src vs q ->
 182  Type src vs t ->
 183  (Qual q ->
 184   Type src vs t ->
 185   Type src vs (q #> t)) ->
 186  Type src vs (q #> t)
 187 tyQual q t f =
 188         case proveConstraint q of
 189          Just Dict -> f Dict t
 190          Nothing -> q #> t
 191 infix 1 `tyQual`
 192
 193 -- ** Type 'TypeK'
 194 -- | Existential 'Type' of a known 'Kind'.
 195 data TypeK src vs kt = forall (t::kt). TypeK (Type src vs t)
 196 type instance SourceOf (TypeK src vs ki) = src
 197 type instance VarsOf (TypeK src vs ki) = vs
 198 instance Source src => Eq (TypeK src vs ki) where
 199         TypeK x == TypeK y = isJust $ eqType x y
 200
 201 -- ** Type 'TypeT'
 202 -- | Existential for 'Type'.
 203 data TypeT src vs = forall t. TypeT (Type src vs t)
 204 type instance SourceOf (TypeT src vs) = src
 205 type instance VarsOf (TypeT src vs) = vs
 206 instance Source src => Eq (TypeT src vs) where
 207         TypeT x == TypeT y = isJust $ eqTypeKi x y
 208
 209 -- ** Type 'TypeVT'
 210 -- | Existential polymorphic 'Type'.
 211 data TypeVT src = forall vs t. TypeVT (Type src vs t)
 212 type instance SourceOf (TypeVT src) = src
 213 instance Source src => Eq (TypeVT src) where
 214         TypeVT x == TypeVT y =
 215                 let (x', y') = appendVars x y in
 216                 isJust $ eqTypeKi x' y'
 217
 218 -- * Type 'Const'
 219 -- | /Type constant/.
 220 data Const src (c::kc) where
 221         Const :: Constable c => Kind src kc -> Const src (c::kc)
 222
 223 type instance SourceOf (Const src c) = src
 224 instance ConstsOf (Const src c) where
 225         constsOf = Set.singleton . ConstC
 226 instance SourceInj (ConstC src) src => KindOf (Const src) where
 227         kindOf c@(Const kc) = kc `withSource` ConstC c
 228
 229 kindOfConst :: Const src (t::kt) -> Kind src kt
 230 kindOfConst (Const kc) = kc
 231
 232 -- ** Class 'Constable'
 233 class
 234  ( Typeable c
 235  , FixityOf c
 236  , NameTyOf c
 237  , ClassInstancesFor c
 238  , TypeInstancesFor c
 239  ) => Constable c
 240 instance
 241  ( Typeable c
 242  , FixityOf c
 243  , NameTyOf c
 244  , ClassInstancesFor c
 245  , TypeInstancesFor c
 246  ) => Constable c
 247
 248 -- ** Class 'ConstsOf'
 249 -- | Return the 'Const's used by something.
 250 class ConstsOf a where
 251         constsOf :: a -> Set (ConstC (SourceOf a))
 252
 253 -- ** Type 'ConstC'
 254 data ConstC src
 255  = forall c. ConstC (Const src c)
 256 instance Eq (ConstC src) where
 257  ConstC x == ConstC y = isJust $ x `eqConstKi` y
 258 instance Ord (ConstC src) where
 259  ConstC x `compare` ConstC y = x `ordConst` y
 260
 261 -- * Type '(->)'
 262 -- | The function 'Type' @(->)@,
 263 -- with an infix notation more readable.
 264 (~>) ::
 265  Source src =>
 266  Constable (->) =>
 267  Type src vs a ->
 268  Type src vs b ->
 269  Type src vs (a -> b)
 270 (~>) a b = (tyConstLen @(K (->)) @(->) (lenVars a) `tyApp` a) `tyApp` b
 271 infixr 0 ~>
 272 instance FixityOf (->) where
 273         fixityOf _c = Just $ Fixity2 $ infixR 0
 274 {- NOTE: defined in Lib.Function
 275 instance ClassInstancesFor (->)
 276 instance TypeInstancesFor  (->)
 277 -}
 278
 279 -- ** Type family 'FunArg'
 280 type family FunArg (fun::K.Type) :: K.Type where
 281         FunArg (q #> f) = FunArg f
 282         FunArg (a -> b) = a
 283
 284 -- ** Type family 'FunRes'
 285 type family FunRes (fun::K.Type) :: K.Type where
 286         FunRes (q #> f) = FunRes f
 287         FunRes (a -> b) = b
 288
 289 -- | Return, when the given 'Type' is a function,
 290 -- the argument of that function.
 291 unTyFun ::
 292  forall t src tys.
 293  SourceInj (TypeVT src) src =>
 294  Constable (->) =>
 295  Type src tys t ->
 296  Maybe ( Type src tys (FunArg t)
 297        , Type src tys (FunRes t) )
 298 unTyFun ty_ini = go ty_ini
 299         where
 300         go ::
 301          Type src tys x ->
 302          Maybe ( Type src tys (FunArg x)
 303                , Type src tys (FunRes x) )
 304         go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
 305          | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
 306          = Just ((a `withSource` TypeVT ty_ini), (b `withSource` TypeVT ty_ini))
 307         go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
 308          | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
 309          = go b
 310         go TyApp{}   = Nothing
 311         go TyConst{} = Nothing
 312         go TyVar{}   = Nothing
 313         go TyFam{}   = Nothing
 314
 315 -- ** Type @(#>)@
 316 -- | /Type constant/ to qualify a 'Type'.
 317 newtype (#>) (q::K.Constraint) (a::K.Type) = Qual (q => a)
 318 instance NameTyOf (#>) where
 319         nameTyOf _c = [] `Mod` "=>"
 320 instance FixityOf (#>) where
 321         fixityOf _c = Just $ Fixity2 $ infixR 0
 322 instance ClassInstancesFor (#>)
 323 instance TypeInstancesFor  (#>)
 324
 325 -- | Qualify a 'Type'.
 326 (#>) ::
 327  Source src =>
 328  Type src vs q ->
 329  Type src vs t ->
 330  Type src vs (q #> t)
 331 (#>) q t = (tyConstLen @(K (#>)) @(#>) (lenVars q) `tyApp` q) `tyApp` t
 332 infixr 0 #>
 333  -- NOTE: should actually be (-1)
 334  -- to compose well with @infixr 0 (->)@
 335  -- but this is not allowed by GHC.
 336
 337 -- ** Class @(#)@
 338 -- | 'K.Constraint' union.
 339 class    (x, y) => x # y
 340 instance (x, y) => x # y
 341 instance NameTyOf (#) where
 342         nameTyOf _c = [] `Mod` ","
 343 instance FixityOf (#) where
 344         fixityOf _c = Just $ Fixity2 $ infixB SideL 0
 345 instance ClassInstancesFor (#) where
 346         proveConstraintFor _c (TyApp _ (TyApp _ c q0) q1)
 347          | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) c
 348          , Just Dict <- proveConstraint q0
 349          , Just Dict <- proveConstraint q1
 350          = Just Dict
 351         proveConstraintFor _c _q = Nothing
 352 instance TypeInstancesFor (#)
 353
 354 -- | Unify two 'K.Constraint's.
 355 (#) ::
 356  Source src =>
 357  Type src vs qx ->
 358  Type src vs qy ->
 359  Type src vs (qx # qy)
 360 (#) a b = (tyConstLen @(K (#)) @(#) (lenVars a) `tyApp` a) `tyApp` b
 361 infixr 2 #
 362
 363 -- ** Type @(() :: @'K.Constraint'@)@
 364 instance NameTyOf (()::K.Constraint) where
 365         nameTyOf _c = [] `Mod` "()"
 366 -- instance FixityOf (()::Constraint)
 367 instance ClassInstancesFor (()::K.Constraint) where
 368         proveConstraintFor _c q
 369          | Just HRefl <- proj_ConstKiTy @K.Constraint @(()::K.Constraint) q
 370          = Just Dict
 371         proveConstraintFor _c _q = Nothing
 372 instance TypeInstancesFor (()::K.Constraint)
 373
 374 -- | Like 'noConstraintLen', but using 'lenInj'.
 375 noConstraint :: Source src => LenInj vs => Type src vs (()::K.Constraint)
 376 noConstraint = tyConstLen @K.Constraint @(()::K.Constraint) lenInj
 377
 378 -- | Empty 'K.Constraint'.
 379 noConstraintLen :: Source src => Len vs -> Type src vs (()::K.Constraint)
 380 noConstraintLen = tyConstLen @K.Constraint @(()::K.Constraint)
 381
 382 -- ** Class @(#~)@
 383 -- | /Type equality/ 'K.Constraint'.
 384 class    (x ~ y) => x #~ y
 385 instance (x ~ y) => x #~ y
 386 instance NameTyOf (#~) where
 387         nameTyOf _c = [] `Mod` "~"
 388         isNameTyOp _c = True
 389 instance FixityOf (#~) where
 390         fixityOf _ = Just $ Fixity2 $ infixB SideL 0
 391 instance
 392  ( KindInj k
 393  , Typeable k
 394  ) => ClassInstancesFor ((#~)::k -> k -> K.Constraint) where
 395         proveConstraintFor _c (TyApp _ (TyApp _ c a) b)
 396          | Just HRefl <- proj_ConstKiTy @(k -> k -> K.Constraint) @(#~) c
 397          , Just Refl  <- eqType a b
 398          = Just Dict
 399         proveConstraintFor _c _q = Nothing
 400 instance TypeInstancesFor  (#~)
 401
 402 -- | Constraint two 'Type's to be equal.
 403 (#~) ::
 404  forall k a b src vs.
 405  Source src =>
 406  Typeable k =>
 407  KindInj k =>
 408  Type src vs (a :: k) ->
 409  Type src vs (b :: k) ->
 410  Type src vs (a #~ b)
 411 (#~) a b = (tyConstLen @(K (#~)) @(#~) (lenVars a) `tyApp` a) `tyApp` b
 412 infixr 2 #~
 413
 414 -- | /Type equality/.
 415 eqType ::
 416  Source src =>
 417  Type src tys (x::k) ->
 418  Type src tys (y::k) ->
 419  Maybe (x:~:y)
 420 eqType x y | Just HRefl <- eqTypeKi x y = Just Refl
 421 eqType _x _y = Nothing
 422
 423 -- | /Heterogeneous type equality/:
 424 -- return two proofs when two 'Type's are equals:
 425 -- one for the type and one for the kind.
 426 eqTypeKi ::
 427  Source src =>
 428  Type src tys (x::kx) ->
 429  Type src tys (y::ky) ->
 430  Maybe (x:~~:y)
 431 eqTypeKi (TyConst _sx _lx x) (TyConst _sy _ly y) = eqConstKi x y
 432 eqTypeKi (TyVar   _sx _nx x) (TyVar   _sy _ny y) = eqVarKi   x y
 433 eqTypeKi (TyApp _sx fx ax) (TyApp _sy fy ay)
 434  | Just HRefl <- eqTypeKi fx fy
 435  , Just HRefl <- eqTypeKi ax ay
 436  = Just HRefl
 437 eqTypeKi (TyFam _ _lx fx ax) (TyFam _ _ly fy ay)
 438  | Just HRefl <- eqConstKi fx fy
 439  , Just HRefl <- eqTypes ax ay
 440  = Just HRefl
 441 -- NOTE: 'TyFam' is expanded as much as possible.
 442 eqTypeKi x@TyFam{} y = eqTypeKi (expandFam x) y
 443 eqTypeKi x y@TyFam{} = eqTypeKi x (expandFam y)
 444 eqTypeKi _x _y = Nothing
 445
 446 eqTypes ::
 447  Source src =>
 448  Types src tys x ->
 449  Types src tys y ->
 450  Maybe (x:~~:y)
 451 eqTypes TypesZ TypesZ = Just HRefl
 452 eqTypes (x `TypesS` sx) (y `TypesS` sy)
 453  | Just HRefl <- eqTypeKi x y
 454  , Just HRefl <- eqTypes sx sy
 455  = Just HRefl
 456 eqTypes _x _y = Nothing
 457
 458 -- *** Comparison
 459 -- | Compare two 'Type's.
 460 ordType ::
 461  Source src =>
 462  Type src tys (x::kx) ->
 463  Type src tys (y::ky) ->
 464  Ordering
 465 -- NOTE: 'TyFam' is expanded as much as possible.
 466 ordType (TyFam _ _lx fx ax) (TyFam _ _ly fy ay) = ordConst fx fy <> ordTypes ax ay
 467 ordType x@TyFam{} y = ordType (expandFam x) y
 468 ordType x y@TyFam{} = ordType x (expandFam y)
 469 ordType (TyConst _sx _lx x) (TyConst _sy _ly y) = ordConst x y
 470 ordType TyConst{} _y = LT
 471 ordType _x TyConst{} = GT
 472 ordType (TyVar _sx _kx x) (TyVar _sy _ky y) = ordVarKi x y
 473 ordType TyVar{} _y = LT
 474 ordType _x TyVar{} = GT
 475 ordType (TyApp _sx fx xx) (TyApp _sy fy xy) = ordType fx fy <> ordType xx xy
 476 -- ordType TyApp{} _y = LT
 477 -- ordType _x TyApp{} = GT
 478
 479 ordTypes ::
 480  Source src =>
 481  Types src tys x ->
 482  Types src tys y ->
 483  Ordering
 484 ordTypes TypesZ TypesZ   = EQ
 485 ordTypes TypesZ TypesS{} = LT
 486 ordTypes TypesS{} TypesZ = GT
 487 ordTypes (x `TypesS` sx) (y `TypesS` sy) = ordType x y <> ordTypes sx sy
 488
 489 -- * Type 'Qual'
 490 -- | Captures the proof of a 'K.Constraint'
 491 -- (and its dictionaries when it contains type classes):
 492 -- pattern matching on the 'Dict' constructor
 493 -- brings the 'K.Constraint' into scope.
 494 data Qual q where
 495         Dict :: q => Qual q
 496
 497 -- ** Class 'ClassInstancesFor'
 498 class ClassInstancesFor c where
 499         proveConstraintFor
 500          :: Source src
 501          => proxy c
 502          -> Type src vs q
 503          -> Maybe (Qual q)
 504         proveConstraintFor _c _q = Nothing
 505
 506 proveConstraint :: Source src => Type src vs q -> Maybe (Qual q)
 507 proveConstraint q = foldr proj Nothing $ constsOf q
 508         where proj (ConstC c@Const{}) = (<|> proveConstraintFor c q)
 509
 510 -- ** Injection
 511 constInj ::
 512  forall c src.
 513  Source src =>
 514  Constable c =>
 515  KindInjP (Ty_of_Type (K c)) =>
 516  Type_of_Ty (Ty_of_Type (K c)) ~ K c =>
 517  Const src c
 518 constInj = Const $ kindInjP @(Ty_of_Type (K c)) noSource
 519
 520 constKiInj ::
 521  forall kc c src.
 522  Source src =>
 523  Constable c =>
 524  Kind src kc ->
 525  Const src (c::kc)
 526 constKiInj = Const
 527
 528 -- ** Projection
 529 {- XXX: not working because of GHC's #12933
 530 proj_ConstKi ::
 531  forall c u src.
 532  Constable c =>
 533  (K c ~ Type_of_Ty (Ty_of_Type (K c))) =>
 534  KindInj (K c) =>
 535  Const src u ->
 536  Maybe (c :~~: u)
 537 proj_ConstKi (Const ku) = do
 538         Refl <- eqKind ku $ kindInj @(K c) @()
 539         Refl :: u:~:c <- eqT
 540         Just HRefl
 541 -}
 542
 543 -- | Like 'proj_ConstKi', but with kind equality already known.
 544 proj_Const ::
 545  forall c u src.
 546  Typeable c =>
 547  Const src u ->
 548  Maybe (c :~: u)
 549 proj_Const Const{} = eqT
 550
 551 -- | Like 'proj_Const', but on a 'Type'.
 552 proj_ConstTy ::
 553  forall c u src vs.
 554  Typeable c =>
 555  Type src vs u ->
 556  Maybe (c :~: u)
 557 proj_ConstTy (TyConst _src _len Const{}) = eqT
 558 proj_ConstTy _ = Nothing
 559
 560 -- | XXX: 'proj_ConstKi' must be given the @kc@ kind explicitely,
 561 -- when used multiple times in the same pattern match,
 562 -- because of GHC's #12933.
 563 proj_ConstKi ::
 564  forall kc (c::kc) u src.
 565  Typeable c =>
 566  (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 567  KindInjP (Ty_of_Type kc) =>
 568  Const src u ->
 569  Maybe (c :~~: u)
 570 proj_ConstKi (Const ku) = do
 571         Refl <- eqKind ku $ kindInjP @(Ty_of_Type kc) ()
 572         Refl :: u:~:c <- eqT
 573         Just HRefl
 574
 575 -- | Like 'proj_ConstKi', but on a 'Type'.
 576 proj_ConstKiTy ::
 577  forall kc (c::kc) u src vs.
 578  Typeable c =>
 579  (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 580  KindInjP (Ty_of_Type kc) =>
 581  Type src vs u ->
 582  Maybe (c :~~: u)
 583 proj_ConstKiTy (TyConst _src _len c) = proj_ConstKi c
 584 proj_ConstKiTy _ = Nothing
 585
 586 eqConst ::
 587  Const src_x (x::k) ->
 588  Const src_y (y::k) ->
 589  Maybe (x:~:y)
 590 eqConst (Const _kx) (Const _ky) = eqT
 591 instance Eq (Const src c) where
 592         x == y = isJust $ eqConstKi x y
 593 instance Ord (Const src c) where
 594         compare = ordConst
 595
 596 eqConstKi ::
 597  forall src_x src_y kx ky x y.
 598  Const src_x (x::kx) ->
 599  Const src_y (y::ky) ->
 600  Maybe (x:~~:y)
 601 eqConstKi (Const kx) (Const ky)
 602  | Just Refl <- eqKind kx ky
 603  , Just (Refl::x:~:y) <- eqT
 604  = Just HRefl
 605 eqConstKi _x _y = Nothing
 606
 607 ordConst ::
 608  forall src_x src_y kx ky x y.
 609  Const src_x (x::kx) ->
 610  Const src_y (y::ky) ->
 611  Ordering
 612 ordConst x@Const{} y@Const{} =
 613         typeRep x `compare` typeRep y
 614
 615 normalizeQualsTy ::
 616  Source src =>
 617  Type src tys (t::kt) ->
 618  TypeK src tys kt
 619 normalizeQualsTy = go
 620         where
 621         go ::
 622          Source src =>
 623          Type src tys (a::ka) ->
 624          TypeK src tys ka
 625         -- (q0, q1)
 626         go (TyApp s1 (TyApp s0 f q0) q1)
 627          | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) f
 628          , TypeK q0' <- go q0
 629          , TypeK q1' <- go q1 =
 630                 case (proveConstraint q0', proveConstraint q1') of
 631                  (Just{}, Just{})  -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q0
 632                  (Just{}, Nothing) -> TypeK q1'
 633                  (Nothing, Just{}) -> TypeK q0'
 634                  (Nothing, Nothing) ->
 635                         case q0' `ordType` q1' of
 636                          LT -> TypeK $ TyApp s1 (TyApp s0 f q0') q1'
 637                          EQ -> TypeK $ q0'
 638                          GT -> TypeK $ TyApp s0 (TyApp s1 f q1') q0'
 639         -- q0 => (q1 => t)
 640         go (TyApp s1 (TyApp s0 f0@(TyConst sf0 lf0 _) q0) (TyApp s2 (TyApp s3 f1 q1) t))
 641          | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f0
 642          , Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f1
 643          , TypeK q0' <- go q0
 644          , TypeK q1' <- go q1 =
 645                 case (proveConstraint q0', proveConstraint q1') of
 646                  (Just{}, Just{})  -> TypeK t
 647                  (Just{}, Nothing) -> TypeK $ TyApp s2 (TyApp s3 f1 q1) t
 648                  (Nothing, Just{}) -> TypeK $ TyApp s1 (TyApp s0 f0 q0) t
 649                  (Nothing, Nothing) ->
 650                         case q0' `ordType` q1' of
 651                          LT ->
 652                                 let q0q1 = TyApp s2 (TyApp s0 (TyConst sf0 lf0 $ constInj @(#)) q0') q1' in
 653                                 TypeK $ TyApp s2 (TyApp s3 f1 q0q1) t
 654                          EQ -> TypeK $ TyApp s2 (TyApp s3 f1 q1') t
 655                          GT ->
 656                                 let q1q0 = TyApp s0 (TyApp s2 (TyConst sf0 lf0 $ constInj @(#)) q1') q0' in
 657                                 TypeK $ TyApp s2 (TyApp s3 f1 q1q0) t
 658         -- q => t
 659         go (TyApp _sa (TyApp _sq (TyConst _sc _lc c) q) t)
 660          | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c =
 661                 case proveConstraint q of
 662                  Just{} -> go t
 663                  Nothing
 664                   | TypeK q' <- go q
 665                   , TypeK t' <- go t
 666                   -> TypeK $ q' #> t'
 667         -- q
 668         go q
 669          | Just Refl <- KiConstraint () `eqKind` kindOfType q
 670          = case proveConstraint q of
 671                  Just{}  -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q
 672                  Nothing -> TypeK q
 673         go (TyApp src f a)
 674          | TypeK f' <- go f
 675          , TypeK a' <- go a
 676          = TypeK $ TyApp src f' a'
 677         go t@TyFam{}   = go (expandFam t)
 678         go t@TyConst{} = TypeK t
 679         go t@TyVar{}   = TypeK t
 680
 681 -- * Type family 'Fam'
 682 -- | Apply the /type family/ selected by @fam@
 683 -- to a list of types (within a 'Proxy').
 684 --
 685 -- | NOTE: |Fam|'s 'Kind' MUST be the same than @fam@'s.
 686 type family Fam (fam::k) (hs::[K.Type]) :: k
 687 -- type family FamKi fam :: K.Type
 688
 689 -- ** Class 'TypeInstancesFor'
 690 class TypeInstancesFor (c::kc) where
 691         expandFamFor
 692          :: Source src
 693          => proxy c
 694          -> Len vs
 695          -> Const src fam
 696          -> Types src vs ts
 697          -> Maybe (Type src vs (Fam fam ts))
 698         expandFamFor _c _len _fam _as = Nothing
 699
 700 -- ** Class 'ExpandFam'
 701 class ExpandFam a where
 702         expandFam :: Source (SourceOf a) => a -> a
 703 instance ExpandFam (Type src vs t) where
 704         expandFam t@TyConst{} = t
 705         expandFam t@TyVar{} = t
 706         expandFam (TyApp src f a) = TyApp src (expandFam f) (expandFam a)
 707         expandFam t@(TyFam _src len fam as) =
 708                 case foldr proj Nothing $ constsOf fam `Set.union` constsOf as of
 709                  Nothing -> t
 710                  Just t' -> expandFam t'
 711                 where proj (ConstC c@Const{}) = (<|> expandFamFor c len fam as)
 712                 -- XXX: this can loop…
 713
 714 -- | Like 'kindOf' but keep the old 'Source'.
 715 kindOfType :: Type src vs (t::kt) -> Kind src kt
 716 kindOfType (TyConst _src _l c) = kindOfConst c
 717 kindOfType (TyApp _src f _a) =
 718         case kindOfType f of
 719          KiFun _src_kf _kx kf -> kf
 720 kindOfType (TyVar _src _n v)         = kindOfVar v
 721 kindOfType (TyFam _src _len fam _as) = kindOfConst fam
 722
 723 -- | Remove unused 'Var's from ther context.
 724 normalizeVarsTy ::
 725  Type src vs (t::kt) ->
 726  (forall vs'. Type src vs' (t::kt) -> ret) -> ret
 727 normalizeVarsTy ty k =
 728         usedVarsOf UsedVarsZ ty $ \vs ->
 729         k $ goTy vs ty
 730         where
 731         goTy ::
 732          UsedVars src vs vs' ->
 733          Type src vs t ->
 734          Type src vs' t
 735         goTy vs (TyConst src _len c) = TyConst src (lenVars vs) c
 736         goTy vs (TyApp src f a)      = TyApp src (goTy vs f) (goTy vs a)
 737         goTy vs (TyVar src n v) =
 738                 case v `lookupUsedVars` vs of
 739                  Nothing -> error "[BUG] normalizeVarsTy: impossible lookup fail"
 740                  Just v' -> TyVar src n v'
 741         goTy vs (TyFam src _len fam as) = TyFam src (lenVars vs) fam $ goTys vs as
 742
 743         goTys ::
 744          UsedVars src vs vs' ->
 745          Types src vs ts ->
 746          Types src vs' ts
 747         goTys _vs TypesZ = TypesZ
 748         goTys vs (TypesS t ts) =
 749                 goTy vs t `TypesS`
 750                 goTys vs ts
 751
 752 -- * Type 'Types'
 753 data Types src vs (ts::[K.Type]) where
 754         TypesZ :: Types src vs '[]
 755         TypesS :: Type src vs t
 756                -> Types src vs ts
 757                -> Types src vs (Proxy t ': ts)
 758 infixr 5 `TypesS`
 759
 760 type instance SourceOf (Types src vs ts) = src
 761 instance ConstsOf (Types src vs ts) where
 762         constsOf TypesZ = Set.empty
 763         constsOf (TypesS t ts) = constsOf t `Set.union` constsOf ts
 764 type instance VarsOf (Types src vs ts) = vs
 765 instance UsedVarsOf (Types src vs ts) where
 766         usedVarsOf vs TypesZ k = k vs
 767         usedVarsOf vs (TypesS t ts) k =
 768                 usedVarsOf vs t $ \vs' ->
 769                 usedVarsOf vs' ts k
 770 instance VarOccursIn (Types src vs ts) where
 771         varOccursIn _v TypesZ = False
 772         varOccursIn v (TypesS t ts) = varOccursIn v t || varOccursIn v ts
 773
 774 mapTys ::
 775  (forall kt (t::kt). Type src vs t -> Type src vs' t) ->
 776  Types src vs  ts ->
 777  Types src vs' ts
 778 mapTys _f TypesZ = TypesZ
 779 mapTys f (TypesS t ts) = f t `TypesS` mapTys f ts
 780
 781 foldlTys ::
 782  (forall k (t::k). Type src vs t -> acc -> acc) ->
 783  Types src vs ts -> acc -> acc
 784 foldlTys _f TypesZ acc = acc
 785 foldlTys f (TypesS t ts) acc = foldlTys f ts (f t acc)
 786
 787 -- * Class 'TypeOf'
 788 class TypeOf a where
 789         typeOf :: a t -> Type (SourceOf (a t)) (VarsOf (a t)) t