symantic/Language/Symantic/Typing/Type.hs

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