symantic/Language/Symantic/Typing/Type.hs

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