mirrored from https://gitlab.haskell.org/ghc/ghc.git
-
Notifications
You must be signed in to change notification settings - Fork 703
/
TyCoRep.hs
2983 lines (2474 loc) · 114 KB
/
TyCoRep.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1998
\section[TyCoRep]{Type and Coercion - friends' interface}
Note [The Type-related module hierarchy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Class
CoAxiom
TyCon imports Class, CoAxiom
TyCoRep imports Class, CoAxiom, TyCon
TysPrim imports TyCoRep ( including mkTyConTy )
Kind imports TysPrim ( mainly for primitive kinds )
Type imports Kind
Coercion imports Type
-}
-- We expose the relevant stuff from this module via the Type module
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE CPP, DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
DeriveTraversable, MultiWayIf #-}
{-# LANGUAGE ImplicitParams #-}
module TyCoRep (
TyThing(..),
Type(..),
TyBinder(..),
TyLit(..),
KindOrType, Kind,
PredType, ThetaType, -- Synonyms
VisibilityFlag(..),
-- * Coercions
Coercion(..), LeftOrRight(..),
UnivCoProvenance(..), CoercionHole(..),
CoercionN, CoercionR, CoercionP, KindCoercion,
-- * Functions over types
mkTyConTy, mkTyVarTy, mkTyVarTys,
mkFunTy, mkFunTys, mkForAllTys,
isLiftedTypeKind, isUnliftedTypeKind,
isCoercionType, isRuntimeRepTy, isRuntimeRepVar,
isRuntimeRepKindedTy, dropRuntimeRepArgs,
sameVis,
-- * Functions over binders
binderType, delBinderVar, isInvisibleBinder, isVisibleBinder,
isNamedBinder, isAnonBinder,
-- * Functions over coercions
pickLR,
-- * Pretty-printing
pprType, pprParendType, pprTypeApp, pprTvBndr, pprTvBndrs,
pprTyThing, pprTyThingCategory, pprSigmaType,
pprTheta, pprForAll, pprForAllImplicit, pprUserForAll,
pprThetaArrowTy, pprClassPred,
pprKind, pprParendKind, pprTyLit,
TyPrec(..), maybeParen, pprTcAppCo, pprTcAppTy,
pprPrefixApp, pprArrowChain, ppr_type,
pprDataCons,
-- * Free variables
tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
tyCoVarsBndrAcc, tyCoVarsOfTypeAcc, tyCoVarsOfTypeList,
tyCoVarsOfTypesAcc, tyCoVarsOfTypesList,
closeOverKindsDSet, closeOverKindsAcc,
coVarsOfType, coVarsOfTypes,
coVarsOfCo, coVarsOfCos,
tyCoVarsOfCo, tyCoVarsOfCos,
tyCoVarsOfCoDSet,
tyCoVarsOfCoAcc, tyCoVarsOfCosAcc,
tyCoVarsOfCoList, tyCoVarsOfProv,
closeOverKinds,
tyCoVarsOfTelescope,
-- * Substitutions
TCvSubst(..), TvSubstEnv, CvSubstEnv,
emptyTvSubstEnv, emptyCvSubstEnv, composeTCvSubstEnv, composeTCvSubst,
emptyTCvSubst, mkEmptyTCvSubst, isEmptyTCvSubst,
mkTCvSubst, mkTvSubst,
getTvSubstEnv,
getCvSubstEnv, getTCvInScope, isInScope, notElemTCvSubst,
setTvSubstEnv, setCvSubstEnv, zapTCvSubst,
extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
extendTCvSubst,
extendCvSubst, extendCvSubstWithClone,
extendTvSubst, extendTvSubstWithClone,
extendTvSubstList, extendTvSubstAndInScope,
extendTvSubstBinder,
unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
zipTvSubst, zipCvSubst,
zipTyBinderSubst,
mkTvSubstPrs,
substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
substCoWith,
substTy, substTyAddInScope,
substTyUnchecked, substTysUnchecked, substThetaUnchecked,
substTyWithBindersUnchecked, substTyWithUnchecked,
substCoUnchecked, substCoWithUnchecked,
substTyWithBinders, substTyWithInScope,
substTys, substTheta,
lookupTyVar, substTyVarBndr,
substCo, substCos, substCoVar, substCoVars, lookupCoVar,
substCoVarBndr, cloneTyVarBndr, cloneTyVarBndrs,
substTyVar, substTyVars,
substForAllCoBndr,
substTyVarBndrCallback, substForAllCoBndrCallback,
substCoVarBndrCallback,
-- * Tidying type related things up for printing
tidyType, tidyTypes,
tidyOpenType, tidyOpenTypes,
tidyOpenKind,
tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars,
tidyOpenTyCoVar, tidyOpenTyCoVars,
tidyTyVarOcc,
tidyTopType,
tidyKind,
tidyCo, tidyCos
) where
#include "HsVersions.h"
import {-# SOURCE #-} DataCon( dataConTyCon, dataConFullSig
, DataCon, eqSpecTyVar )
import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy
, tyCoVarsOfTypesWellScoped, varSetElemsWellScoped
, partitionInvisibles, coreView, typeKind )
-- Transitively pulls in a LOT of stuff, better to break the loop
import {-# SOURCE #-} Coercion
import {-# SOURCE #-} ConLike ( ConLike(..) )
-- friends:
import Var
import VarEnv
import VarSet
import Name hiding ( varName )
import BasicTypes
import TyCon
import Class
import CoAxiom
import FV
-- others
import PrelNames
import Binary
import Outputable
import DynFlags
import StaticFlags ( opt_PprStyle_Debug )
import FastString
import Pair
import UniqSupply
import ListSetOps
import Util
import UniqFM
-- libraries
import qualified Data.Data as Data hiding ( TyCon )
import Data.List
import Data.IORef ( IORef ) -- for CoercionHole
#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
import GHC.Stack (CallStack)
#endif
{-
%************************************************************************
%* *
\subsection{The data type}
%* *
%************************************************************************
-}
-- | The key representation of types within the compiler
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
data Type
-- See Note [Non-trivial definitional equality]
= TyVarTy Var -- ^ Vanilla type or kind variable (*never* a coercion variable)
| AppTy -- See Note [AppTy rep]
Type
Type -- ^ Type application to something other than a 'TyCon'. Parameters:
--
-- 1) Function: must /not/ be a 'TyConApp',
-- must be another 'AppTy', or 'TyVarTy'
--
-- 2) Argument type
| TyConApp -- See Note [AppTy rep]
TyCon
[KindOrType] -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
-- Invariant: saturated applications of 'FunTyCon' must
-- use 'FunTy' and saturated synonyms must use their own
-- constructors. However, /unsaturated/ 'FunTyCon's
-- do appear as 'TyConApp's.
-- Parameters:
--
-- 1) Type constructor being applied to.
--
-- 2) Type arguments. Might not have enough type arguments
-- here to saturate the constructor.
-- Even type synonyms are not necessarily saturated;
-- for example unsaturated type synonyms
-- can appear as the right hand side of a type synonym.
| ForAllTy
TyBinder
Type -- ^ A Π type.
-- This includes arrow types, constructed with
-- @ForAllTy (Anon ...)@. See also Note [TyBinder].
| LitTy TyLit -- ^ Type literals are similar to type constructors.
| CastTy
Type
KindCoercion -- ^ A kind cast. The coercion is always nominal.
-- INVARIANT: The cast is never refl.
-- INVARIANT: The cast is "pushed down" as far as it
-- can go. See Note [Pushing down casts]
| CoercionTy
Coercion -- ^ Injection of a Coercion into a type
-- This should only ever be used in the RHS of an AppTy,
-- in the list of a TyConApp, when applying a promoted
-- GADT data constructor
deriving (Data.Data, Data.Typeable)
-- NOTE: Other parts of the code assume that type literals do not contain
-- types or type variables.
data TyLit
= NumTyLit Integer
| StrTyLit FastString
deriving (Eq, Ord, Data.Data, Data.Typeable)
-- | A 'TyBinder' represents an argument to a function. TyBinders can be dependent
-- ('Named') or nondependent ('Anon'). They may also be visible or not.
-- See also Note [TyBinder]
data TyBinder
= Named TyVar VisibilityFlag -- Always a TyVar (not CoVar or Id)
| Anon Type -- Visibility is determined by the type (Constraint vs. *)
deriving (Data.Typeable, Data.Data)
-- | Is something required to appear in source Haskell ('Visible'),
-- permitted by request ('Specified') (visible type application), or
-- prohibited entirely from appearing in source Haskell ('Invisible')?
-- Examples in Note [VisibilityFlag]
data VisibilityFlag = Visible | Specified | Invisible
deriving (Eq, Data.Typeable, Data.Data)
-- | Do these denote the same level of visibility? Except that
-- 'Specified' and 'Invisible' are considered the same. Used
-- for printing.
sameVis :: VisibilityFlag -> VisibilityFlag -> Bool
sameVis Visible Visible = True
sameVis Visible _ = False
sameVis _ Visible = False
sameVis _ _ = True
instance Binary VisibilityFlag where
put_ bh Visible = putByte bh 0
put_ bh Specified = putByte bh 1
put_ bh Invisible = putByte bh 2
get bh = do
h <- getByte bh
case h of
0 -> return Visible
1 -> return Specified
_ -> return Invisible
type KindOrType = Type -- See Note [Arguments to type constructors]
-- | The key type representing kinds in the compiler.
type Kind = Type
{-
Note [TyBinder]
~~~~~~~~~~~~~~~
This represents the type of binders -- that is, the type of an argument
to a Pi-type. GHC Core currently supports two different Pi-types:
a non-dependent function, written with ->, and a dependent compile-time-only
polytype, written with forall. Both Pi-types classify terms/types that
take an argument. In other words, if `x` is either a function or a polytype,
`x arg` makes sense (for an appropriate `arg`). It is thus often convenient
to group Pi-types together. This is ForAllTy.
The two constructors for TyBinder sort out the two different possibilities.
`Named` builds a polytype, while `Anon` builds an ordinary function.
(ForAllTy (Anon arg) res used to be called FunTy arg res.)
Note [The kind invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~
The kinds
# UnliftedTypeKind
OpenKind super-kind of *, #
can never appear under an arrow or type constructor in a kind; they
can only be at the top level of a kind. It follows that primitive TyCons,
which have a naughty pseudo-kind
State# :: * -> #
must always be saturated, so that we can never get a type whose kind
has a UnliftedTypeKind or ArgTypeKind underneath an arrow.
Nor can we abstract over a type variable with any of these kinds.
k :: = kk | # | ArgKind | (#) | OpenKind
kk :: = * | kk -> kk | T kk1 ... kkn
So a type variable can only be abstracted kk.
Note [Arguments to type constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Because of kind polymorphism, in addition to type application we now
have kind instantiation. We reuse the same notations to do so.
For example:
Just (* -> *) Maybe
Right * Nat Zero
are represented by:
TyConApp (PromotedDataCon Just) [* -> *, Maybe]
TyConApp (PromotedDataCon Right) [*, Nat, (PromotedDataCon Zero)]
Important note: Nat is used as a *kind* and not as a type. This can be
confusing, since type-level Nat and kind-level Nat are identical. We
use the kind of (PromotedDataCon Right) to know if its arguments are
kinds or types.
This kind instantiation only happens in TyConApp currently.
Note [Pushing down casts]
~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have (a :: k1 -> *), (b :: k1), and (co :: * ~ q).
The type (a b |> co) is `eqType` to ((a |> co') b), where
co' = (->) <k1> co. Thus, to make this visible to functions
that inspect types, we always push down coercions, preferring
the second form. Note that this also applies to TyConApps!
Note [Non-trivial definitional equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Is Int |> <*> the same as Int? YES! In order to reduce headaches,
we decide that any reflexive casts in types are just ignored. More
generally, the `eqType` function, which defines Core's type equality
relation, ignores casts and coercion arguments, as long as the
two types have the same kind. This allows us to be a little sloppier
in keeping track of coercions, which is a good thing. It also means
that eqType does not depend on eqCoercion, which is also a good thing.
Note [VisibilityFlag]
~~~~~~~~~~~~~~~~~~~~~
All named binders are equipped with a visibility flag, which says
whether or not arguments for this binder should be visible (explicit)
in source Haskell. Historically, all named binders (that is, polytype
binders) have been Invisible. But now it's more complicated.
Invisible:
Argument does not ever appear in source Haskell. With visible type
application, only GHC-generated polytypes have Invisible binders.
This exactly corresponds to "generalized" variables from the
Visible Type Applications paper (ESOP'16).
Example: f x = x
`f` will be inferred to have type `forall a. a -> a`, where `a` is
Invisible. Note that there is no type annotation for `f`.
Printing: With -fprint-explicit-foralls, Invisible binders are written
in braces. Otherwise, they are printed like Specified binders.
Specified:
The argument for this binder may appear in source Haskell only with
visible type application. Otherwise, it is omitted.
Example: id :: forall a. a -> a
`a` is a Specified binder, because you can say `id @Int` in source Haskell.
Example: const :: a -> b -> a
Both `a` and `b` are Specified binders, even though they are not bound
by an explicit forall.
Printing: a list of Specified binders are put between `forall` and `.`:
const :: forall a b. a -> b -> a
Visible:
The argument must be given. Visible binders come up only with TypeInType.
Example: data Proxy k (a :: k) = P
The kind of Proxy is forall k -> k -> *, where k is a Visible binder.
Printing: As in the example above, Visible binders are put between `forall`
and `->`. This syntax is not parsed (yet), however.
-------------------------------------
Note [PredTy]
-}
-- | A type of the form @p@ of kind @Constraint@ represents a value whose type is
-- the Haskell predicate @p@, where a predicate is what occurs before
-- the @=>@ in a Haskell type.
--
-- We use 'PredType' as documentation to mark those types that we guarantee to have
-- this kind.
--
-- It can be expanded into its representation, but:
--
-- * The type checker must treat it as opaque
--
-- * The rest of the compiler treats it as transparent
--
-- Consider these examples:
--
-- > f :: (Eq a) => a -> Int
-- > g :: (?x :: Int -> Int) => a -> Int
-- > h :: (r\l) => {r} => {l::Int | r}
--
-- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
type PredType = Type
-- | A collection of 'PredType's
type ThetaType = [PredType]
{-
(We don't support TREX records yet, but the setup is designed
to expand to allow them.)
A Haskell qualified type, such as that for f,g,h above, is
represented using
* a FunTy for the double arrow
* with a type of kind Constraint as the function argument
The predicate really does turn into a real extra argument to the
function. If the argument has type (p :: Constraint) then the predicate p is
represented by evidence of type p.
%************************************************************************
%* *
Simple constructors
%* *
%************************************************************************
These functions are here so that they can be used by TysPrim,
which in turn is imported by Type
-}
-- named with "Only" to prevent naive use of mkTyVarTy
mkTyVarTy :: TyVar -> Type
mkTyVarTy v = ASSERT2( isTyVar v, ppr v <+> dcolon <+> ppr (tyVarKind v) )
TyVarTy v
mkTyVarTys :: [TyVar] -> [Type]
mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
infixr 3 `mkFunTy` -- Associates to the right
-- | Make an arrow type
mkFunTy :: Type -> Type -> Type
mkFunTy arg res = ForAllTy (Anon arg) res
-- | Make nested arrow types
mkFunTys :: [Type] -> Type -> Type
mkFunTys tys ty = foldr mkFunTy ty tys
-- | Wraps foralls over the type using the provided 'TyVar's from left to right
mkForAllTys :: [TyBinder] -> Type -> Type
mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
-- | Does this type classify a core Coercion?
isCoercionType :: Type -> Bool
isCoercionType (TyConApp tc tys)
| (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
, length tys == 4
= True
isCoercionType _ = False
binderType :: TyBinder -> Type
binderType (Named v _) = varType v
binderType (Anon ty) = ty
-- | Remove the binder's variable from the set, if the binder has
-- a variable.
delBinderVar :: VarSet -> TyBinder -> VarSet
delBinderVar vars (Named tv _) = vars `delVarSet` tv
delBinderVar vars (Anon {}) = vars
-- | Remove the binder's variable from the set, if the binder has
-- a variable.
delBinderVarFV :: TyBinder -> FV -> FV
delBinderVarFV (Named tv _) vars fv_cand in_scope acc = delFV tv vars fv_cand in_scope acc
delBinderVarFV (Anon {}) vars fv_cand in_scope acc = vars fv_cand in_scope acc
-- | Does this binder bind an invisible argument?
isInvisibleBinder :: TyBinder -> Bool
isInvisibleBinder (Named _ vis) = vis /= Visible
isInvisibleBinder (Anon ty) = isPredTy ty
-- | Does this binder bind a visible argument?
isVisibleBinder :: TyBinder -> Bool
isVisibleBinder = not . isInvisibleBinder
isNamedBinder :: TyBinder -> Bool
isNamedBinder (Named {}) = True
isNamedBinder _ = False
isAnonBinder :: TyBinder -> Bool
isAnonBinder (Anon {}) = True
isAnonBinder _ = False
-- | Create the plain type constructor type which has been applied to no type arguments at all.
mkTyConTy :: TyCon -> Type
mkTyConTy tycon = TyConApp tycon []
{-
Some basic functions, put here to break loops eg with the pretty printer
-}
-- | This version considers Constraint to be distinct from *.
isLiftedTypeKind :: Kind -> Bool
isLiftedTypeKind ki | Just ki' <- coreView ki = isLiftedTypeKind ki'
isLiftedTypeKind (TyConApp tc [TyConApp ptr_rep []])
= tc `hasKey` tYPETyConKey
&& ptr_rep `hasKey` ptrRepLiftedDataConKey
isLiftedTypeKind _ = False
isUnliftedTypeKind :: Kind -> Bool
isUnliftedTypeKind ki | Just ki' <- coreView ki = isUnliftedTypeKind ki'
isUnliftedTypeKind (TyConApp tc [TyConApp ptr_rep []])
| tc `hasKey` tYPETyConKey
, ptr_rep `hasKey` ptrRepLiftedDataConKey
= False
isUnliftedTypeKind (TyConApp tc [arg])
= tc `hasKey` tYPETyConKey && isEmptyVarSet (tyCoVarsOfType arg)
-- all other possibilities are unlifted
isUnliftedTypeKind _ = False
-- | Is this the type 'RuntimeRep'?
isRuntimeRepTy :: Type -> Bool
isRuntimeRepTy ty | Just ty' <- coreView ty = isRuntimeRepTy ty'
isRuntimeRepTy (TyConApp tc []) = tc `hasKey` runtimeRepTyConKey
isRuntimeRepTy _ = False
-- | Is this a type of kind RuntimeRep? (e.g. PtrRep)
isRuntimeRepKindedTy :: Type -> Bool
isRuntimeRepKindedTy = isRuntimeRepTy . typeKind
-- | Is a tyvar of type 'RuntimeRep'?
isRuntimeRepVar :: TyVar -> Bool
isRuntimeRepVar = isRuntimeRepTy . tyVarKind
-- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g.
-- dropping 'PtrRep arguments of unboxed tuple TyCon applications:
--
-- dropRuntimeRepArgs [ 'PtrRepLifted, 'PtrRepUnlifted
-- , String, Int# ] == [String, Int#]
--
dropRuntimeRepArgs :: [Type] -> [Type]
dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy
{-
%************************************************************************
%* *
Coercions
%* *
%************************************************************************
-}
-- | A 'Coercion' is concrete evidence of the equality/convertibility
-- of two types.
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
data Coercion
-- Each constructor has a "role signature", indicating the way roles are
-- propagated through coercions.
-- - P, N, and R stand for coercions of the given role
-- - e stands for a coercion of a specific unknown role
-- (think "role polymorphism")
-- - "e" stands for an explicit role parameter indicating role e.
-- - _ stands for a parameter that is not a Role or Coercion.
-- These ones mirror the shape of types
= -- Refl :: "e" -> _ -> e
Refl Role Type -- See Note [Refl invariant]
-- Invariant: applications of (Refl T) to a bunch of identity coercions
-- always show up as Refl.
-- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)).
-- Applications of (Refl T) to some coercions, at least one of
-- which is NOT the identity, show up as TyConAppCo.
-- (They may not be fully saturated however.)
-- ConAppCo coercions (like all coercions other than Refl)
-- are NEVER the identity.
-- Use (Refl Representational _), not (SubCo (Refl Nominal _))
-- These ones simply lift the correspondingly-named
-- Type constructors into Coercions
-- TyConAppCo :: "e" -> _ -> ?? -> e
-- See Note [TyConAppCo roles]
| TyConAppCo Role TyCon [Coercion] -- lift TyConApp
-- The TyCon is never a synonym;
-- we expand synonyms eagerly
-- But it can be a type function
| AppCo Coercion CoercionN -- lift AppTy
-- AppCo :: e -> N -> e
-- See Note [Forall coercions]
| ForAllCo TyVar KindCoercion Coercion
-- ForAllCo :: _ -> N -> e -> e
-- These are special
| CoVarCo CoVar -- :: _ -> (N or R)
-- result role depends on the tycon of the variable's type
-- AxiomInstCo :: e -> _ -> [N] -> e
| AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
-- See also [CoAxiom index]
-- The coercion arguments always *precisely* saturate
-- arity of (that branch of) the CoAxiom. If there are
-- any left over, we use AppCo.
-- See [Coercion axioms applied to coercions]
| UnivCo UnivCoProvenance Role Type Type
-- :: _ -> "e" -> _ -> _ -> e
| SymCo Coercion -- :: e -> e
| TransCo Coercion Coercion -- :: e -> e -> e
-- The number coercions should match exactly the expectations
-- of the CoAxiomRule (i.e., the rule is fully saturated).
| AxiomRuleCo CoAxiomRule [Coercion]
| NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
-- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles])
-- Using NthCo on a ForAllCo gives an N coercion always
-- See Note [NthCo and newtypes]
| LRCo LeftOrRight CoercionN -- Decomposes (t_left t_right)
-- :: _ -> N -> N
| InstCo Coercion CoercionN
-- :: e -> N -> e
-- See Note [InstCo roles]
-- Coherence applies a coercion to the left-hand type of another coercion
-- See Note [Coherence]
| CoherenceCo Coercion KindCoercion
-- :: e -> N -> e
-- Extract a kind coercion from a (heterogeneous) type coercion
-- NB: all kind coercions are Nominal
| KindCo Coercion
-- :: e -> N
| SubCo CoercionN -- Turns a ~N into a ~R
-- :: N -> R
deriving (Data.Data, Data.Typeable)
type CoercionN = Coercion -- always nominal
type CoercionR = Coercion -- always representational
type CoercionP = Coercion -- always phantom
type KindCoercion = CoercionN -- always nominal
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
data LeftOrRight = CLeft | CRight
deriving( Eq, Data.Data, Data.Typeable )
instance Binary LeftOrRight where
put_ bh CLeft = putByte bh 0
put_ bh CRight = putByte bh 1
get bh = do { h <- getByte bh
; case h of
0 -> return CLeft
_ -> return CRight }
pickLR :: LeftOrRight -> (a,a) -> a
pickLR CLeft (l,_) = l
pickLR CRight (_,r) = r
{-
Note [Refl invariant]
~~~~~~~~~~~~~~~~~~~~~
Invariant 1:
Coercions have the following invariant
Refl is always lifted as far as possible.
You might think that a consequencs is:
Every identity coercions has Refl at the root
But that's not quite true because of coercion variables. Consider
g where g :: Int~Int
Left h where h :: Maybe Int ~ Maybe Int
etc. So the consequence is only true of coercions that
have no coercion variables.
Note [Coercion axioms applied to coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The reason coercion axioms can be applied to coercions and not just
types is to allow for better optimization. There are some cases where
we need to be able to "push transitivity inside" an axiom in order to
expose further opportunities for optimization.
For example, suppose we have
C a : t[a] ~ F a
g : b ~ c
and we want to optimize
sym (C b) ; t[g] ; C c
which has the kind
F b ~ F c
(stopping through t[b] and t[c] along the way).
We'd like to optimize this to just F g -- but how? The key is
that we need to allow axioms to be instantiated by *coercions*,
not just by types. Then we can (in certain cases) push
transitivity inside the axiom instantiations, and then react
opposite-polarity instantiations of the same axiom. In this
case, e.g., we match t[g] against the LHS of (C c)'s kind, to
obtain the substitution a |-> g (note this operation is sort
of the dual of lifting!) and hence end up with
C g : t[b] ~ F c
which indeed has the same kind as t[g] ; C c.
Now we have
sym (C b) ; C g
which can be optimized to F g.
Note [CoAxiom index]
~~~~~~~~~~~~~~~~~~~~
A CoAxiom has 1 or more branches. Each branch has contains a list
of the free type variables in that branch, the LHS type patterns,
and the RHS type for that branch. When we apply an axiom to a list
of coercions, we must choose which branch of the axiom we wish to
use, as the different branches may have different numbers of free
type variables. (The number of type patterns is always the same
among branches, but that doesn't quite concern us here.)
The Int in the AxiomInstCo constructor is the 0-indexed number
of the chosen branch.
Note [Forall coercions]
~~~~~~~~~~~~~~~~~~~~~~~
Constructing coercions between forall-types can be a bit tricky,
because the kinds of the bound tyvars can be different.
The typing rule is:
kind_co : k1 ~ k2
tv1:k1 |- co : t1 ~ t2
-------------------------------------------------------------------
ForAllCo tv1 kind_co co : all tv1:k1. t1 ~
all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co])
First, the TyVar stored in a ForAllCo is really an optimisation: this field
should be a Name, as its kind is redundant. Thinking of the field as a Name
is helpful in understanding what a ForAllCo means.
The idea is that kind_co gives the two kinds of the tyvar. See how, in the
conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right.
Of course, a type variable can't have different kinds at the same time. So,
we arbitrarily prefer the first kind when using tv1 in the inner coercion
co, which shows that t1 equals t2.
The last wrinkle is that we need to fix the kinds in the conclusion. In
t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of
the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with
(tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it
mentions the same name with different kinds, but it *is* well-kinded, noting
that `(tv1:k2) |> sym kind_co` has kind k1.
This all really would work storing just a Name in the ForAllCo. But we can't
add Names to, e.g., VarSets, and there generally is just an impedence mismatch
in a bunch of places. So we use tv1. When we need tv2, we can use
setTyVarKind.
Note [Coherence]
~~~~~~~~~~~~~~~~
The Coherence typing rule is thus:
g1 : s ~ t s : k1 g2 : k1 ~ k2
------------------------------------
CoherenceCo g1 g2 : (s |> g2) ~ t
While this looks (and is) unsymmetric, a combination of other coercion
combinators can make the symmetric version.
For role information, see Note [Roles and kind coercions].
Note [Predicate coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
g :: a~b
How can we coerce between types
([c]~a) => [a] -> c
and
([c]~b) => [b] -> c
where the equality predicate *itself* differs?
Answer: we simply treat (~) as an ordinary type constructor, so these
types really look like
((~) [c] a) -> [a] -> c
((~) [c] b) -> [b] -> c
So the coercion between the two is obviously
((~) [c] g) -> [g] -> c
Another way to see this to say that we simply collapse predicates to
their representation type (see Type.coreView and Type.predTypeRep).
This collapse is done by mkPredCo; there is no PredCo constructor
in Coercion. This is important because we need Nth to work on
predicates too:
Nth 1 ((~) [c] g) = g
See Simplify.simplCoercionF, which generates such selections.
Note [Roles]
~~~~~~~~~~~~
Roles are a solution to the GeneralizedNewtypeDeriving problem, articulated
in Trac #1496. The full story is in docs/core-spec/core-spec.pdf. Also, see
http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation
Here is one way to phrase the problem:
Given:
newtype Age = MkAge Int
type family F x
type instance F Age = Bool
type instance F Int = Char
This compiles down to:
axAge :: Age ~ Int
axF1 :: F Age ~ Bool
axF2 :: F Int ~ Char
Then, we can make:
(sym (axF1) ; F axAge ; axF2) :: Bool ~ Char
Yikes!
The solution is _roles_, as articulated in "Generative Type Abstraction and
Type-level Computation" (POPL 2010), available at
http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf
The specification for roles has evolved somewhat since that paper. For the
current full details, see the documentation in docs/core-spec. Here are some
highlights.
We label every equality with a notion of type equivalence, of which there are
three options: Nominal, Representational, and Phantom. A ground type is
nominally equivalent only with itself. A newtype (which is considered a ground
type in Haskell) is representationally equivalent to its representation.
Anything is "phantomly" equivalent to anything else. We use "N", "R", and "P"
to denote the equivalences.
The axioms above would be:
axAge :: Age ~R Int
axF1 :: F Age ~N Bool
axF2 :: F Age ~N Char
Then, because transitivity applies only to coercions proving the same notion
of equivalence, the above construction is impossible.
However, there is still an escape hatch: we know that any two types that are
nominally equivalent are representationally equivalent as well. This is what
the form SubCo proves -- it "demotes" a nominal equivalence into a
representational equivalence. So, it would seem the following is possible:
sub (sym axF1) ; F axAge ; sub axF2 :: Bool ~R Char -- WRONG
What saves us here is that the arguments to a type function F, lifted into a
coercion, *must* prove nominal equivalence. So, (F axAge) is ill-formed, and
we are safe.
Roles are attached to parameters to TyCons. When lifting a TyCon into a
coercion (through TyConAppCo), we need to ensure that the arguments to the
TyCon respect their roles. For example:
data T a b = MkT a (F b)
If we know that a1 ~R a2, then we know (T a1 b) ~R (T a2 b). But, if we know
that b1 ~R b2, we know nothing about (T a b1) and (T a b2)! This is because
the type function F branches on b's *name*, not representation. So, we say
that 'a' has role Representational and 'b' has role Nominal. The third role,
Phantom, is for parameters not used in the type's definition. Given the
following definition
data Q a = MkQ Int
the Phantom role allows us to say that (Q Bool) ~R (Q Char), because we
can construct the coercion Bool ~P Char (using UnivCo).
See the paper cited above for more examples and information.
Note [TyConAppCo roles]
~~~~~~~~~~~~~~~~~~~~~~~
The TyConAppCo constructor has a role parameter, indicating the role at
which the coercion proves equality. The choice of this parameter affects
the required roles of the arguments of the TyConAppCo. To help explain
it, assume the following definition:
type instance F Int = Bool -- Axiom axF : F Int ~N Bool
newtype Age = MkAge Int -- Axiom axAge : Age ~R Int
data Foo a = MkFoo a -- Role on Foo's parameter is Representational
TyConAppCo Nominal Foo axF : Foo (F Int) ~N Foo Bool
For (TyConAppCo Nominal) all arguments must have role Nominal. Why?
So that Foo Age ~N Foo Int does *not* hold.
TyConAppCo Representational Foo (SubCo axF) : Foo (F Int) ~R Foo Bool
TyConAppCo Representational Foo axAge : Foo Age ~R Foo Int
For (TyConAppCo Representational), all arguments must have the roles
corresponding to the result of tyConRoles on the TyCon. This is the
whole point of having roles on the TyCon to begin with. So, we can
have Foo Age ~R Foo Int, if Foo's parameter has role R.
If a Representational TyConAppCo is over-saturated (which is otherwise fine),
the spill-over arguments must all be at Nominal. This corresponds to the
behavior for AppCo.
TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool
All arguments must have role Phantom. This one isn't strictly
necessary for soundness, but this choice removes ambiguity.
The rules here dictate the roles of the parameters to mkTyConAppCo
(should be checked by Lint).
Note [NthCo and newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
newtype N a = MkN Int
type role N representational
This yields axiom
NTCo:N :: forall a. N a ~R Int
We can then build
co :: forall a b. N a ~R N b
co = NTCo:N a ; sym (NTCo:N b)
for any `a` and `b`. Because of the role annotation on N, if we use
NthCo, we'll get out a representational coercion. That is:
NthCo 0 co :: forall a b. a ~R b
Yikes! Clearly, this is terrible. The solution is simple: forbid
NthCo to be used on newtypes if the internal coercion is representational.
This is not just some corner case discovered by a segfault somewhere;
it was discovered in the proof of soundness of roles and described
in the "Safe Coercions" paper (ICFP '14).
Note [InstCo roles]
~~~~~~~~~~~~~~~~~~~
Here is (essentially) the typing rule for InstCo:
g :: (forall a. t1) ~r (forall a. t2)
w :: s1 ~N s2
------------------------------- InstCo
InstCo g w :: (t1 [a |-> s1]) ~r (t2 [a |-> s2])
Note that the Coercion w *must* be nominal. This is necessary
because the variable a might be used in a "nominal position"
(that is, a place where role inference would require a nominal
role) in t1 or t2. If we allowed w to be representational, we
could get bogus equalities.
A more nuanced treatment might be able to relax this condition
somewhat, by checking if t1 and/or t2 use their bound variables
in nominal ways. If not, having w be representational is OK.
%************************************************************************
%* *