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' 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 using 'noSource' and 'inj_Const'.
 140 --
 141 -- FIXME: remove @kc@ when GHC's #12933 is fixed.
 142 tyConstLen ::
 143  forall kc (c::kc) src vs.
 144  Source src =>
 145  Constable c =>
 146  Inj_KindP (Ty_of_Type kc) =>
 147  Type_of_Ty (Ty_of_Type kc) ~ kc =>
 148  Len vs ->
 149  Type src vs c
 150 tyConstLen len = TyConst noSource len inj_Const
 151
 152 -- | Like 'TyApp', but using 'noSource'.
 153 tyApp ::
 154  Source src =>
 155  Type src vs f ->
 156  Type src vs a ->
 157  Type src vs (f a)
 158 tyApp = TyApp noSource
 159 infixl 9 `tyApp`
 160
 161 -- | Like 'TyVar', but using 'noSource'.
 162 tyVar ::
 163  Source src =>
 164  NameVar ->
 165  Var src vs v ->
 166  Type src vs v
 167 tyVar = TyVar noSource
 168
 169 -- | Like 'TyFam', but using 'noSource'.
 170 --
 171 -- FIXME: remove @kc@ when GHC's #12933 is fixed.
 172 tyFam ::
 173  forall kc (c::kc) as vs src.
 174  Source src =>
 175  Inj_Len vs =>
 176  Constable c =>
 177  Inj_KindP (Ty_of_Type kc) =>
 178  Type_of_Ty (Ty_of_Type kc) ~ kc =>
 179  Types src vs as ->
 180  Type src vs (Fam c as)
 181 tyFam = TyFam noSource inj_Len (inj_Const @c)
 182
 183 -- | Qualify a 'Type'.
 184 tyQual ::
 185  Source src =>
 186  Type src vs q ->
 187  Type src vs t ->
 188  (Qual q ->
 189   Type src vs t ->
 190   Type src vs (q #> t)) ->
 191  Type src vs (q #> t)
 192 tyQual q t f =
 193         case proveConstraint q of
 194          Just Dict -> f Dict t
 195          Nothing -> q #> t
 196 infix 1 `tyQual`
 197
 198 -- ** Type 'TypeK'
 199 -- | Existential 'Type' of a known 'Kind'.
 200 data TypeK src vs kt = forall (t::kt). TypeK (Type src vs t)
 201 type instance SourceOf (TypeK src vs ki) = src
 202 type instance VarsOf (TypeK src vs ki) = vs
 203 instance Source src => Eq (TypeK src vs ki) where
 204         TypeK x == TypeK y = isJust $ eqType x y
 205
 206 -- ** Type 'TypeT'
 207 -- | Existential for 'Type'.
 208 data TypeT src vs = forall t. TypeT (Type src vs t)
 209 type instance SourceOf (TypeT src vs) = src
 210 type instance VarsOf (TypeT src vs) = vs
 211 instance Source src => Eq (TypeT src vs) where
 212         TypeT x == TypeT y = isJust $ eqTypeKi x y
 213
 214 -- ** Type 'TypeVT'
 215 -- | Existential polymorphic 'Type'.
 216 data TypeVT src = forall vs t. TypeVT (Type src vs t)
 217 type instance SourceOf (TypeVT src) = src
 218 instance Source src => Eq (TypeVT src) where
 219         TypeVT x == TypeVT y =
 220                 let (x', y') = appendVars x y in
 221                 isJust $ eqTypeKi x' y'
 222
 223 -- * Type 'Const'
 224 -- | /Type constant/.
 225 data Const src (c::kc) where
 226         Const :: Constable c
 227               => Kind src kc
 228               -> Const src (c::kc)
 229
 230 type instance SourceOf (Const src c) = src
 231 instance ConstsOf (Const src c) where
 232         constsOf = Set.singleton . ConstC
 233 instance Inj_Source (ConstC src) src => KindOf (Const src) where
 234         kindOf c@(Const kc) = kc `source` ConstC c
 235
 236 kindOfConst :: Const src (t::kt) -> Kind src kt
 237 kindOfConst (Const kc) = kc
 238
 239 -- ** Class 'Constable'
 240 class
 241  ( Typeable c
 242  , FixityOf c
 243  , ClassInstancesFor c
 244  , TypeInstancesFor c
 245  ) => Constable c
 246 instance
 247  ( Typeable c
 248  , FixityOf c
 249  , ClassInstancesFor c
 250  , TypeInstancesFor c
 251  ) => Constable c
 252
 253 -- ** Class 'ConstsOf'
 254 -- | Return the 'Const's used by something.
 255 class ConstsOf a where
 256         constsOf :: a -> Set (ConstC (SourceOf a))
 257
 258 -- ** Class 'FixityOf'
 259 -- | Return the 'Fixity' of something.
 260 class FixityOf (c::kc) where
 261         fixityOf :: proxy c -> Maybe Fixity
 262         fixityOf _c = Nothing
 263 instance FixityOf (c::K.Type)
 264 instance FixityOf (c::K.Constraint)
 265
 266 -- Show
 267 instance Show (Const src c) where
 268         showsPrec p c@Const{} = showsPrec p $ typeRep c
 269
 270 -- ** Type 'ConstC'
 271 data ConstC src
 272  = forall c. ConstC (Const src c)
 273 instance Eq (ConstC src) where
 274  ConstC x == ConstC y = isJust $ x `eqConstKi` y
 275 instance Ord (ConstC src) where
 276  ConstC x `compare` ConstC y = x `ordConst` y
 277
 278 -- * Type '(->)'
 279 -- | The function 'Type' @(->)@,
 280 -- with an infix notation more readable.
 281 (~>) ::
 282  Source src =>
 283  Constable (->) =>
 284  Type src vs a ->
 285  Type src vs b ->
 286  Type src vs (a -> b)
 287 (~>) a b = (tyConstLen @(K (->)) @(->) (lenVars a) `tyApp` a) `tyApp` b
 288 infixr 0 ~>
 289 instance FixityOf (->) where
 290         fixityOf _c = Just $ Fixity2 $ infixR 0
 291 {- NOTE: defined in Lib.Function
 292 instance ClassInstancesFor (->)
 293 instance TypeInstancesFor  (->)
 294 -}
 295
 296 -- ** Type family 'FunArg'
 297 type family FunArg (fun::K.Type) :: K.Type where
 298         FunArg (q #> f) = FunArg f
 299         FunArg (a -> b) = a
 300
 301 -- ** Type family 'FunRes'
 302 type family FunRes (fun::K.Type) :: K.Type where
 303         FunRes (q #> f) = FunRes f
 304         FunRes (a -> b) = b
 305
 306 -- | Return, when the given 'Type' is a function,
 307 -- the argument of that function.
 308 unTyFun ::
 309  forall t src tys.
 310  Inj_Source (TypeVT src) src =>
 311  Constable (->) =>
 312  Type src tys t ->
 313  Maybe ( Type src tys (FunArg t)
 314        , Type src tys (FunRes t) )
 315 unTyFun ty_ini = go ty_ini
 316         where
 317         go ::
 318          Type src tys x ->
 319          Maybe ( Type src tys (FunArg x)
 320                , Type src tys (FunRes x) )
 321         go (TyApp _ (TyApp _ (TyConst _ _ f) a) b)
 322          | Just HRefl <- proj_ConstKi @(K (->)) @(->) f
 323          = Just ((a `source` TypeVT ty_ini), (b `source` TypeVT ty_ini))
 324         go (TyApp _ (TyApp _ (TyConst _ _ f) _a) b)
 325          | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f
 326          = go b
 327         go TyApp{}   = Nothing
 328         go TyConst{} = Nothing
 329         go TyVar{}   = Nothing
 330         go TyFam{}   = Nothing
 331
 332 -- ** Type @(#>)@
 333 -- | /Type constant/ to qualify a 'Type'.
 334 newtype (#>) (q::K.Constraint) (a::K.Type) = Qual (q => a)
 335 instance FixityOf (#>) where
 336         fixityOf _c = Just $ Fixity2 $ infixR 0
 337 instance ClassInstancesFor (#>)
 338 instance TypeInstancesFor  (#>)
 339
 340 (#>) ::
 341  Source src =>
 342  Type src vs a ->
 343  Type src vs b ->
 344  Type src vs (a #> b)
 345 (#>) a b = (tyConstLen @(K (#>)) @(#>) (lenVars a) `tyApp` a) `tyApp` b
 346 infixr 0 #>
 347  -- NOTE: should actually be (-1)
 348  -- to compose well with @infixr 0 (->)@
 349  -- but this is not allowed by GHC.
 350
 351 -- ** Class @(#)@
 352 -- | 'K.Constraint' union.
 353 class    (x, y) => x # y
 354 instance (x, y) => x # y
 355 instance FixityOf (#) where
 356         fixityOf _c = Just $ Fixity2 $ infixB SideL 0
 357 instance ClassInstancesFor (#) where
 358         proveConstraintFor _c (TyApp _ (TyApp _ c q0) q1)
 359          | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) c
 360          , Just Dict <- proveConstraint q0
 361          , Just Dict <- proveConstraint q1
 362          = Just Dict
 363         proveConstraintFor _c _q = Nothing
 364 instance TypeInstancesFor (#)
 365
 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 (#~) ::
 411  forall k a b src vs.
 412  Source src =>
 413  Typeable k =>
 414  Inj_Kind k =>
 415  Type src vs (a :: k) ->
 416  Type src vs (b :: k) ->
 417  Type src vs (a #~ b)
 418 (#~) a b = (tyConstLen @(K (#~)) @(#~) (lenVars a) `tyApp` a) `tyApp` b
 419 infixr 2 #~
 420
 421 {-
 422 const_EqTy ::
 423  forall k src.
 424  Source src =>
 425  Typeable k =>
 426  Inj_Kind k =>
 427  Const src ((#~)::k -> k -> K.Constraint)
 428 const_EqTy = inj_Const @(#~)
 429 -}
 430
 431 -- | /Type equality/.
 432 eqType ::
 433  Source src =>
 434  Type src tys (x::k) ->
 435  Type src tys (y::k) ->
 436  Maybe (x:~:y)
 437 eqType x y | Just HRefl <- eqTypeKi x y = Just Refl
 438 eqType _x _y = Nothing
 439
 440 -- | /Heterogeneous type equality/:
 441 -- return two proofs when two 'Type's are equals:
 442 -- one for the type and one for the kind.
 443 eqTypeKi ::
 444  Source src =>
 445  Type src tys (x::kx) ->
 446  Type src tys (y::ky) ->
 447  Maybe (x:~~:y)
 448 eqTypeKi (TyConst _sx _lx x) (TyConst _sy _ly y) = eqConstKi x y
 449 eqTypeKi (TyVar   _sx _nx x) (TyVar   _sy _ny y) = eqVarKi   x y
 450 eqTypeKi (TyApp _sx fx ax) (TyApp _sy fy ay)
 451  | Just HRefl <- eqTypeKi fx fy
 452  , Just HRefl <- eqTypeKi ax ay
 453  = Just HRefl
 454 eqTypeKi (TyFam _ _lx fx ax) (TyFam _ _ly fy ay)
 455  | Just HRefl <- eqConstKi fx fy
 456  , Just HRefl <- eqTypes ax ay
 457  = Just HRefl
 458 -- NOTE: 'TyFam' is expanded as much as possible.
 459 eqTypeKi x@TyFam{} y = eqTypeKi (expandFam x) y
 460 eqTypeKi x y@TyFam{} = eqTypeKi x (expandFam y)
 461 eqTypeKi _x _y = Nothing
 462
 463 eqTypes ::
 464  Source src =>
 465  Types src tys x ->
 466  Types src tys y ->
 467  Maybe (x:~~:y)
 468 eqTypes TypesZ TypesZ = Just HRefl
 469 eqTypes (x `TypesS` sx) (y `TypesS` sy)
 470  | Just HRefl <- eqTypeKi x y
 471  , Just HRefl <- eqTypes sx sy
 472  = Just HRefl
 473 eqTypes _x _y = Nothing
 474
 475 -- *** Comparison
 476 -- | Compare two 'Type's.
 477 ordType ::
 478  Source src =>
 479  Type src tys (x::kx) ->
 480  Type src tys (y::ky) ->
 481  Ordering
 482 -- NOTE: 'TyFam' is expanded as much as possible.
 483 ordType (TyFam _ _lx fx ax) (TyFam _ _ly fy ay) = ordConst fx fy <> ordTypes ax ay
 484 ordType x@TyFam{} y = ordType (expandFam x) y
 485 ordType x y@TyFam{} = ordType x (expandFam y)
 486 ordType (TyConst _sx _lx x) (TyConst _sy _ly y) = ordConst x y
 487 ordType TyConst{} _y = LT
 488 ordType _x TyConst{} = GT
 489 ordType (TyVar _sx _kx x) (TyVar _sy _ky y) = ordVarKi x y
 490 ordType TyVar{} _y = LT
 491 ordType _x TyVar{} = GT
 492 ordType (TyApp _sx fx xx) (TyApp _sy fy xy) = ordType fx fy <> ordType xx xy
 493 -- ordType TyApp{} _y = LT
 494 -- ordType _x TyApp{} = GT
 495
 496 ordTypes ::
 497  Source src =>
 498  Types src tys x ->
 499  Types src tys y ->
 500  Ordering
 501 ordTypes TypesZ TypesZ   = EQ
 502 ordTypes TypesZ TypesS{} = LT
 503 ordTypes TypesS{} TypesZ = GT
 504 ordTypes (x `TypesS` sx) (y `TypesS` sy) = ordType x y <> ordTypes sx sy
 505
 506 -- * Type 'Qual'
 507 -- | Captures the proof of a 'K.Constraint'
 508 -- (and its dictionaries when it contains type classes):
 509 -- pattern matching on the 'Dict' constructor
 510 -- brings the 'K.Constraint' into scope.
 511 data Qual q where
 512         Dict :: q => Qual q
 513
 514 -- ** Class 'ClassInstancesFor'
 515 class ClassInstancesFor c where
 516         proveConstraintFor
 517          :: Source src
 518          => proxy c
 519          -> Type src vs q
 520          -> Maybe (Qual q)
 521         proveConstraintFor _c _q = Nothing
 522
 523 proveConstraint :: Source src => Type src vs q -> Maybe (Qual q)
 524 proveConstraint q = foldr proj Nothing $ constsOf q
 525         where proj (ConstC c@Const{}) = (<|> proveConstraintFor c q)
 526
 527 -- ** Injection
 528 inj_Const ::
 529  forall c src.
 530  Source src =>
 531  Constable c =>
 532  Inj_KindP (Ty_of_Type (K c)) =>
 533  Type_of_Ty (Ty_of_Type (K c)) ~ K c =>
 534  Const src c
 535 inj_Const = Const $ inj_KindP @(Ty_of_Type (K c)) noSource
 536
 537 inj_ConstKi ::
 538  forall kc c src.
 539  Source src =>
 540  Constable c =>
 541  Kind src kc ->
 542  Const src (c::kc)
 543 inj_ConstKi = Const
 544
 545 -- ** Projection
 546 {- XXX: not working because of GHC's #12933
 547 proj_ConstKi ::
 548  forall c u src.
 549  Constable c =>
 550  (K c ~ Type_of_Ty (Ty_of_Type (K c))) =>
 551  Inj_Kind (K c) =>
 552  Const src u ->
 553  Maybe (c :~~: u)
 554 proj_ConstKi (Const ku) = do
 555         Refl <- eqKind ku $ inj_Kind @(K c) @()
 556         Refl :: u:~:c <- eqT
 557         Just HRefl
 558 -}
 559
 560 -- | Like 'proj_ConstKi', but with kind equality already known.
 561 proj_Const ::
 562  forall c u src.
 563  Typeable c =>
 564  Const src u ->
 565  Maybe (c :~: u)
 566 proj_Const Const{} = eqT
 567
 568 -- | Like 'proj_Const', but on a 'Type'.
 569 proj_ConstTy ::
 570  forall c u src vs.
 571  Typeable c =>
 572  Type src vs u ->
 573  Maybe (c :~: u)
 574 proj_ConstTy (TyConst _src _len Const{}) = eqT
 575 proj_ConstTy _ = Nothing
 576
 577 -- | XXX: 'proj_ConstKi' must be given the @kc@ kind explicitely,
 578 -- when used multiple times in the same pattern match,
 579 -- because of GHC's #12933.
 580 proj_ConstKi ::
 581  forall kc (c::kc) u src.
 582  Typeable c =>
 583  (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 584  Inj_KindP (Ty_of_Type kc) =>
 585  Const src u ->
 586  Maybe (c :~~: u)
 587 proj_ConstKi (Const ku) = do
 588         Refl <- eqKind ku $ inj_KindP @(Ty_of_Type kc) ()
 589         Refl :: u:~:c <- eqT
 590         Just HRefl
 591
 592 -- | Like 'proj_ConstKi', but on a 'Type'.
 593 proj_ConstKiTy ::
 594  forall kc (c::kc) u src vs.
 595  Typeable c =>
 596  (kc ~ Type_of_Ty (Ty_of_Type kc)) =>
 597  Inj_KindP (Ty_of_Type kc) =>
 598  Type src vs u ->
 599  Maybe (c :~~: u)
 600 proj_ConstKiTy (TyConst _src _len c) = proj_ConstKi c
 601 proj_ConstKiTy _ = Nothing
 602
 603 eqConst ::
 604  Const src_x (x::k) ->
 605  Const src_y (y::k) ->
 606  Maybe (x:~:y)
 607 eqConst (Const _kx) (Const _ky) = eqT
 608 instance Eq (Const src c) where
 609         x == y = isJust $ eqConstKi x y
 610 instance Ord (Const src c) where
 611         compare = ordConst
 612
 613 eqConstKi ::
 614  forall src_x src_y kx ky x y.
 615  Const src_x (x::kx) ->
 616  Const src_y (y::ky) ->
 617  Maybe (x:~~:y)
 618 eqConstKi (Const kx) (Const ky)
 619  | Just Refl <- eqKind kx ky
 620  , Just (Refl::x:~:y) <- eqT
 621  = Just HRefl
 622 eqConstKi _x _y = Nothing
 623
 624 ordConst ::
 625  forall src_x src_y kx ky x y.
 626  Const src_x (x::kx) ->
 627  Const src_y (y::ky) ->
 628  Ordering
 629 ordConst x@Const{} y@Const{} =
 630         typeRep x `compare` typeRep y
 631
 632 normalizeQualsTy ::
 633  Source src =>
 634  Type src tys (t::kt) ->
 635  TypeK src tys kt
 636 normalizeQualsTy = go
 637         where
 638         go ::
 639          Source src =>
 640          Type src tys (a::ka) ->
 641          TypeK src tys ka
 642         -- (q0, q1)
 643         go (TyApp s1 (TyApp s0 f q0) q1)
 644          | Just HRefl <- proj_ConstKiTy @(K (#)) @(#) f
 645          , TypeK q0' <- go q0
 646          , TypeK q1' <- go q1 =
 647                 case (proveConstraint q0', proveConstraint q1') of
 648                  (Just{}, Just{})  -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q0
 649                  (Just{}, Nothing) -> TypeK q1'
 650                  (Nothing, Just{}) -> TypeK q0'
 651                  (Nothing, Nothing) ->
 652                         case q0' `ordType` q1' of
 653                          LT -> TypeK $ TyApp s1 (TyApp s0 f q0') q1'
 654                          EQ -> TypeK $ q0'
 655                          GT -> TypeK $ TyApp s0 (TyApp s1 f q1') q0'
 656         -- q0 => (q1 => t)
 657         go (TyApp s1 (TyApp s0 f0@(TyConst sf0 lf0 _) q0) (TyApp s2 (TyApp s3 f1 q1) t))
 658          | Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f0
 659          , Just HRefl <- proj_ConstKiTy @(K (#>)) @(#>) f1
 660          , TypeK q0' <- go q0
 661          , TypeK q1' <- go q1 =
 662                 case (proveConstraint q0', proveConstraint q1') of
 663                  (Just{}, Just{})  -> TypeK t
 664                  (Just{}, Nothing) -> TypeK $ TyApp s2 (TyApp s3 f1 q1) t
 665                  (Nothing, Just{}) -> TypeK $ TyApp s1 (TyApp s0 f0 q0) t
 666                  (Nothing, Nothing) ->
 667                         case q0' `ordType` q1' of
 668                          LT ->
 669                                 let q0q1 = TyApp s2 (TyApp s0 (TyConst sf0 lf0 $ inj_Const @(#)) q0') q1' in
 670                                 TypeK $ TyApp s2 (TyApp s3 f1 q0q1) t
 671                          EQ -> TypeK $ TyApp s2 (TyApp s3 f1 q1') t
 672                          GT ->
 673                                 let q1q0 = TyApp s0 (TyApp s2 (TyConst sf0 lf0 $ inj_Const @(#)) q1') q0' in
 674                                 TypeK $ TyApp s2 (TyApp s3 f1 q1q0) t
 675         -- q => t
 676         go (TyApp _sa (TyApp _sq (TyConst _sc _lc c) q) t)
 677          | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c =
 678                 case proveConstraint q of
 679                  Just{} -> go t
 680                  Nothing
 681                   | TypeK q' <- go q
 682                   , TypeK t' <- go t
 683                   -> TypeK $ q' #> t'
 684         -- q
 685         go q
 686          | Just Refl <- KiConstraint () `eqKind` kindOfType q
 687          = case proveConstraint q of
 688                  Just{}  -> TypeK $ tyConstLen @K.Constraint @(()::K.Constraint) $ lenVars q
 689                  Nothing -> TypeK q
 690         go (TyApp src f a)
 691          | TypeK f' <- go f
 692          , TypeK a' <- go a
 693          = TypeK $ TyApp src f' a'
 694         go t@TyFam{}   = go (expandFam t)
 695         go t@TyConst{} = TypeK t
 696         go t@TyVar{}   = TypeK t
 697
 698 -- * Type family 'Fam'
 699 -- | Apply the /type family/ selected by @fam@
 700 -- to a list of types (within a 'Proxy').
 701 --
 702 -- | NOTE: |Fam|'s 'Kind' MUST be the same than @fam@'s.
 703 type family Fam (fam::k) (hs::[K.Type]) :: k
 704 -- type family FamKi fam :: K.Type
 705
 706 -- ** Class 'TypeInstancesFor'
 707 class TypeInstancesFor (c::kc) where
 708         expandFamFor
 709          :: Source src
 710          => proxy c
 711          -> Len vs
 712          -> Const src fam
 713          -> Types src vs ts
 714          -> Maybe (Type src vs (Fam fam ts))
 715         expandFamFor _c _len _fam _as = Nothing
 716
 717 -- ** Class 'ExpandFam'
 718 class ExpandFam a where
 719         expandFam :: Source (SourceOf a) => a -> a
 720 instance ExpandFam (Type src vs t) where
 721         expandFam t@TyConst{} = t
 722         expandFam t@TyVar{} = t
 723         expandFam (TyApp src f a) = TyApp src (expandFam f) (expandFam a)
 724         expandFam t@(TyFam _src len fam as) =
 725                 case foldr proj Nothing $ constsOf fam `Set.union` constsOf as of
 726                  Nothing -> t
 727                  Just t' -> expandFam t'
 728                 where proj (ConstC c@Const{}) = (<|> expandFamFor c len fam as)
 729                 -- XXX: this can loop…
 730
 731 -- | Like 'kindOf' but keep the old 'Source'.
 732 kindOfType :: Type src vs (t::kt) -> Kind src kt
 733 kindOfType (TyConst _src _l c) = kindOfConst c
 734 kindOfType (TyApp _src f _a) =
 735         case kindOfType f of
 736          KiFun _src_kf _kx kf -> kf
 737 kindOfType (TyVar _src _n v)         = kindOfVar v
 738 kindOfType (TyFam _src _len fam _as) = kindOfConst fam
 739
 740 -- | Remove unused 'Var's from ther context.
 741 normalizeVarsTy ::
 742  Type src vs (t::kt) ->
 743  (forall vs'. Type src vs' (t::kt) -> ret) -> ret
 744 normalizeVarsTy ty k =
 745         usedVarsOf UsedVarsZ ty $ \vs ->
 746         k $ goTy vs ty
 747         where
 748         goTy ::
 749          UsedVars src vs vs' ->
 750          Type src vs t ->
 751          Type src vs' t
 752         goTy vs (TyConst src _len c) = TyConst src (lenVars vs) c
 753         goTy vs (TyApp src f a)      = TyApp src (goTy vs f) (goTy vs a)
 754         goTy vs (TyVar src n v) =
 755                 case v `lookupUsedVars` vs of
 756                  Nothing -> error "[BUG] normalizeVarsTy: impossible lookup fail"
 757                  Just v' -> TyVar src n v'
 758         goTy vs (TyFam src _len fam as) = TyFam src (lenVars vs) fam $ goTys vs as
 759
 760         goTys ::
 761          UsedVars src vs vs' ->
 762          Types src vs ts ->
 763          Types src vs' ts
 764         goTys _vs TypesZ = TypesZ
 765         goTys vs (TypesS t ts) =
 766                 goTy vs t `TypesS`
 767                 goTys vs ts
 768
 769 -- * Type 'Types'
 770 data Types src vs (ts::[K.Type]) where
 771         TypesZ :: Types src vs '[]
 772         TypesS :: Type src vs t
 773                -> Types src vs ts
 774                -> Types src vs (Proxy t ': ts)
 775 infixr 5 `TypesS`
 776
 777 type instance SourceOf (Types src vs ts) = src
 778 instance ConstsOf (Types src vs ts) where
 779         constsOf TypesZ = Set.empty
 780         constsOf (TypesS t ts) = constsOf t `Set.union` constsOf ts
 781 type instance VarsOf (Types src vs ts) = vs
 782 instance UsedVarsOf (Types src vs ts) where
 783         usedVarsOf vs TypesZ k = k vs
 784         usedVarsOf vs (TypesS t ts) k =
 785                 usedVarsOf vs t $ \vs' ->
 786                 usedVarsOf vs' ts k
 787 instance VarOccursIn (Types src vs ts) where
 788         varOccursIn _v TypesZ = False
 789         varOccursIn v (TypesS t ts) = varOccursIn v t || varOccursIn v ts
 790
 791 mapTys ::
 792  (forall kt (t::kt). Type src vs t -> Type src vs' t) ->
 793  Types src vs  ts ->
 794  Types src vs' ts
 795 mapTys _f TypesZ = TypesZ
 796 mapTys f (TypesS t ts) = f t `TypesS` mapTys f ts
 797
 798 foldlTys ::
 799  (forall k (t::k). Type src vs t -> acc -> acc) ->
 800  Types src vs ts -> acc -> acc
 801 foldlTys _f TypesZ acc = acc
 802 foldlTys f (TypesS t ts) acc = foldlTys f ts (f t acc)
 803
 804 -- * Class 'TypeOf'
 805 class TypeOf a where
 806         typeOf :: a t -> Type (SourceOf (a t)) (VarsOf (a t)) t