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