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