symantic/Language/Symantic/Typing/Type.hs

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