never executed always true always false
1 {-# LANGUAGE MultiWayIf #-}
2
3 module GHC.Tc.Utils.Concrete
4 ( -- * Creating/emitting 'Concrete#' constraints
5 hasFixedRuntimeRep
6 , newConcretePrimWanted
7 -- * HsWrapper: checking for representation-polymorphism
8 , mkWpFun
9 )
10 where
11
12 import GHC.Prelude
13
14 import GHC.Core.Coercion
15 import GHC.Core.TyCo.Rep
16
17 import GHC.Tc.Utils.Monad
18 import GHC.Tc.Utils.TcType ( TcType, mkTyConApp )
19 import GHC.Tc.Utils.TcMType ( newCoercionHole, newFlexiTyVarTy )
20 import GHC.Tc.Types.Constraint
21 import GHC.Tc.Types.Evidence
22 import GHC.Tc.Types.Origin ( CtOrigin(..), FRROrigin(..), WpFunOrigin(..) )
23
24 import GHC.Builtin.Types ( unliftedTypeKindTyCon, liftedTypeKindTyCon )
25 import GHC.Builtin.Types.Prim ( concretePrimTyCon )
26
27 import GHC.Types.Basic ( TypeOrKind(KindLevel) )
28
29 import GHC.Core.Type ( isConcrete, typeKind )
30
31 {- Note [Concrete overview]
32 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
33 Special predicates of the form `Concrete# ty` are used
34 to check, in the typechecker, that certain types have a fixed runtime representation.
35 We give here an overview of the various moving parts, to serve
36 as a central point of reference for this topic.
37
38 * Representation polymorphism
39 Note [Representation polymorphism invariants] in GHC.Core
40 Note [Representation polymorphism checking]
41
42 The first note explains why we require that certain types have
43 a fixed runtime representation.
44
45 The second note details why we sometimes need a constraint to
46 perform such checks in the typechecker: we might not know immediately
47 whether a type has a fixed runtime representation. For example, we might
48 need further unification to take place before being able to decide.
49 So, instead of checking immediately, we emit a constraint.
50
51 * What does it mean for a type to be concrete?
52 Note [Concrete types]
53 Note [The Concrete mechanism]
54
55 The predicate 'Concrete# ty' is satisfied when we can produce
56 a coercion
57
58 co :: ty ~ concrete_ty
59
60 where 'concrete_ty' consists only of concrete types (no type variables,
61 no type families).
62
63 The first note explains more precisely what it means for a type to be concrete.
64 The second note explains how this relates to the `Concrete#` predicate,
65 and explains that the implementation is happening in two phases (PHASE 1 and PHASE 2).
66 In PHASE 1 (the current implementation) we only allow trivial evidence
67 of the form `co = Refl`.
68
69 * Fixed runtime representation vs fixed RuntimeRep
70 Note [Fixed RuntimeRep]
71
72 We currently enforce the representation-polymorphism invariants by checking
73 that binders and function arguments have a "fixed RuntimeRep".
74 That is, `ty :: ki` has a "fixed RuntimeRep" if we can solve `Concrete# ki`.
75
76 This is slightly less general than we might like, as this rules out
77 types with kind `TYPE (BoxedRep l)`: we know that this will be represented
78 by a pointer, which should be enough to go on in many situations.
79
80 * When do we emit 'Concrete#' constraints?
81 Note [hasFixedRuntimeRep]
82
83 We introduce 'Concrete#' constraints to satisfy the representation-polymorphism
84 invariants outlined in Note [Representation polymorphism invariants] in GHC.Core,
85 which mostly amounts to the following two cases:
86
87 - checking that a binder has a fixed runtime representation,
88 - checking that a function argument has a fixed runtime representation.
89
90 The note explains precisely how we emit these 'Concrete#' constraints.
91
92 * How do we solve Concrete# constraints?
93 Note [Solving Concrete# constraints] in GHC.Tc.Instance.Class
94
95 Concrete# constraints are solved through two mechanisms,
96 which are both explained further in the note:
97
98 - by decomposing them, e.g. `Concrete# (TYPE r)` is turned
99 into `Concrete# r` (canonicalisation of `Concrete#` constraints),
100 - by using 'Concrete' instances (top-level interactions).
101 The note explains that the evidence we get from using such 'Concrete'
102 instances can only ever be Refl, even in PHASE 2.
103
104 * Reporting unsolved Concrete# constraints
105 Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin
106
107 When we emit a 'Concrete#' constraint, we also provide a 'FRROrigin'
108 which gives context about the check being done. This origin gets reported
109 to the user if we end up with an unsolved Wanted 'Concrete#' constraint.
110
111 Note [Representation polymorphism checking]
112 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
113 According to the "Levity Polymorphism" paper (PLDI '17),
114 there are two places in which we must know that a type has a
115 fixed runtime representation, as explained in
116 Note [Representation polymorphism invariants] in GHC.Core:
117
118 I1. the type of a bound term-level variable,
119 I2. the type of an argument to a function.
120
121 The paper explains the restrictions more fully, but briefly:
122 expressions in these contexts need to be stored in registers, and it's
123 hard (read: impossible) to store something that does not have a
124 fixed runtime representation.
125
126 In practice, we enforce these types to have a /fixed RuntimeRep/, which is slightly
127 stronger, as explained in Note [Fixed RuntimeRep].
128
129 There are two different ways we check whether a given type
130 has a fixed runtime representation, both in the typechecker:
131
132 1. When typechecking type declarations (e.g. datatypes, typeclass, pattern synonyms),
133 under the GHC.Tc.TyCl module hierarchy.
134 In these situations, we can immediately reject bad representation polymorphism.
135
136 For instance, the following datatype declaration
137
138 data Foo (r :: RuntimeRep) (a :: TYPE r) = Foo a
139
140 is rejected in GHC.Tc.TyCl.checkValidDataCon upon seeing that the type 'a'
141 is representation-polymorphic.
142
143 Such checks are done using `GHC.Tc.Utils.TcMType.checkTypeHasFixedRuntimeRep`,
144 with `GHC.Tc.Errors.Types.FixedRuntimeRepProvenance` describing the different
145 contexts in which bad representation polymorphism can occur while validity checking.
146
147 2. When typechecking value-level declarations (functions, expressions, patterns, ...),
148 under the GHC.Tc.Gen module hierarchy.
149 In these situations, the typechecker might need to do some work to figure out
150 whether a type has a fixed runtime representation or not. For instance,
151 GHC might introduce a metavariable (rr :: RuntimeRep), which is only later
152 (through constraint solving) discovered to be equal to FloatRep.
153
154 This is handled by the Concrete mechanism outlined in
155 Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.
156 See Note [Concrete overview] in GHC.Tc.Utils.Concrete for an overview
157 of the various moving parts.
158
159 The idea is that, to guarantee that a type (rr :: RuntimeRep) is
160 representation-monomorphic, we emit a 'Concrete# rr' Wanted constraint.
161 If GHC can solve this constraint, it means 'rr' is monomorphic, and we
162 are OK to proceed. Otherwise, we report this unsolved Wanted in the form
163 of a representation-polymorphism error. The different contexts in which
164 such constraints arise are enumerated in 'FRROrigin'.
165
166 Note [Concrete types]
167 ~~~~~~~~~~~~~~~~~~~~~
168 Definition: a type is /concrete/
169 iff it consists of a tree of concrete type constructors
170 See GHC.Core.Type.isConcrete
171
172 Definition: a /concrete type constructor/ is defined by
173 - a promoted data constructor
174 - a class, data type or newtype
175 - a primitive type like Array# or Int#
176 - an abstract type as defined in a Backpack signature file
177 (see Note [Synonyms implement abstract data] in GHC.Tc.Module)
178 In particular, type and data families are not concrete.
179 See GHC.Core.TyCon.isConcreteTyCon.
180
181 Examples of concrete types:
182 Lifted, BoxedRep Lifted, TYPE (BoxedRep Lifted) are all concrete
183 Examples of non-concrete types
184 F Int, TYPE (F Int), TYPE r, a Int
185 NB: (F Int) is not concrete because F is a type function
186
187 Note [The Concrete mechanism]
188 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
189 As explained in (2) in Note [Representation polymorphism checking],
190 to check (ty :: ki) has a fixed runtime representation,
191 we emit a `Concrete# ki` constraint, where
192
193 Concrete# :: forall k. k -> TupleRep '[]
194
195 Such constraints get solved by decomposition, as per
196 Note [Canonical Concrete# constraints] in GHC.Tc.Solver.Canonical.
197 When unsolved Wanted `Concrete#` constraints remain after typechecking,
198 we report them as representation-polymorphism errors, using `GHC.Tc.Types.Origin.FRROrigin`
199 to inform the user of the context in which a fixed-runtime-rep check arose.
200
201 --------------
202 -- EVIDENCE --
203 --------------
204
205 The evidence for a 'Concrete# ty' constraint is a nominal coercion
206
207 co :: ty ~# concrete_ty
208
209 where 'concrete_ty' consists only of (non-synonym) type constructors and applications
210 (after expanding any vanilla type synonyms).
211
212 OK:
213
214 TYPE FloatRep
215 TYPE (BoxedRep Lifted)
216 Type
217 TYPE (TupleRep '[ FloatRep, SumRep '[ IntRep, IntRep ] ])
218
219 Not OK:
220
221 Type variables:
222
223 ty
224 TYPE r
225 TYPE (BoxedRep l)
226
227 Type family applications:
228
229 TYPE (Id FloatRep)
230
231 This is so that we can compute the 'PrimRep's needed to represent the type
232 using 'runtimeRepPrimRep', which expects to be able to read off the 'RuntimeRep',
233 as per Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType.
234
235 Note that the evidence for a `Concrete#` constraint isn't a typeclass dictionary:
236 like with `(~#)`, the evidence is an (unlifted) nominal coercion, which justifies defining
237
238 Concrete# :: forall k. k -> TYPE (TupleRep '[])
239
240 We still need a constraint that users can write in their own programs,
241 so much like `(~#)` and `(~)` we also define:
242
243 Concrete :: forall k. k -> Constraint
244
245 The need for user-facing 'Concrete' constraints is detailed in
246 Note [Concrete and Concrete#] in GHC.Builtin.Types.
247
248 -------------------------
249 -- PHASE 1 and PHASE 2 --
250 -------------------------
251
252 The Concrete mechanism is being implemented in two separate phases.
253
254 In PHASE 1 (currently implemented), we never allow a 'Concrete#' constraint
255 to be rewritten (see e.g. GHC.Tc.Solver.Canonical.canConcretePrim).
256 The only allowable evidence term is Refl, which forbids any program
257 that requires type family evaluation in order to determine that a 'RuntimeRep' is fixed.
258 N.B.: we do not currently check that this invariant is upheld: as we are discarding the
259 evidence in PHASE 1, we no longer have access to the coercion after constraint solving
260 (which is the point at which we would want to check that the filled in evidence is Refl).
261
262 In PHASE 2 (future work), we lift this restriction. To illustrate what this entails,
263 recall that the code generator needs to be able to compute 'PrimRep's, so that it
264 can put function arguments in the correct registers, etc.
265 As a result, we must insert additional casts in Core to ensure that no type family
266 reduction is needed to be able to compute 'PrimRep's. For example, the Core
267
268 f = /\ ( a :: F Int ). \ ( x :: a ). some_expression
269
270 is problematic when 'F' is a type family: we don't know what runtime representation to use
271 for 'x', so we can't compile this function (we can't evaluate type family applications
272 after we are done with typechecking). Instead, we ensure the 'RuntimeRep' is always
273 explicitly visible:
274
275 f = /\ ( a :: F Int ). \ ( x :: ( a |> kco ) ). some_expression
276
277 where 'kco' is the evidence for `Concrete# (F Int)`, for example if `F Int = TYPE Int#`
278 this would be:
279
280 kco :: F Int ~# TYPE Int#
281
282 As `( a |> kco ) :: TYPE Int#`, the code generator knows to use a machine-sized
283 integer register for `x`, and all is good again.
284
285 Example test cases that require PHASE 2: T13105, T17021, T20363b.
286
287 Note [Fixed RuntimeRep]
288 ~~~~~~~~~~~~~~~~~~~~~~~
289 Definition:
290 a type `ty :: ki` has a /fixed RuntimeRep/
291 iff we can solve `Concrete# ki`
292
293 In PHASE 1 (see Note [The Concrete mechanism]), this is equivalent to:
294
295 a type `ty :: ki` has a /fixed RuntimeRep/
296 iff `ki` is a concrete type (in the sense of Note [Concrete types]).
297
298 This definition is crafted to be useful to satisfy the invariants of
299 Core; see Note [Representation polymorphism invariants] in GHC.Core.
300
301 Notice that "fixed RuntimeRep" means (for now anyway) that
302 * we know the runtime representation, and
303 * we know the levity.
304
305 For example (ty :: TYPE (BoxedRep l)), where `l` is a levity variable
306 is /not/ "fixed RuntimeRep", even though it is always represented by
307 a heap pointer, because we don't know the levity. In due course we
308 will want to make finer distinctions, as explained in the paper
309 Kinds are Calling Conventions [ICFP'20], but this suffices for now.
310
311 Note [hasFixedRuntimeRep]
312 ~~~~~~~~~~~~~~~~~~~~~~~~~
313 The 'hasFixedRuntimeRep' function is responsible for taking a type 'ty'
314 and emitting a 'Concrete#' constraint to ensure that 'ty' has a fixed `RuntimeRep`,
315 as outlined in Note [The Concrete mechanism].
316
317 To do so, we compute the kind 'ki' of 'ty' and emit a 'Concrete# ki' constraint,
318 which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRep.
319
320 [Wrinkle: Typed Template Haskell]
321 We don't perform any checks when type-checking a typed Template Haskell quote:
322 we want to allow representation polymorphic quotes, as long as they are
323 monomorphised at splice site.
324
325 Example:
326
327 Module1
328
329 repPolyId :: forall r (a :: TYPE r). CodeQ (a -> a)
330 repPolyId = [|| \ x -> x ||]
331
332 Module2
333
334 import Module1
335
336 id1 :: Int -> Int
337 id1 = $$repPolyId
338
339 id2 :: Int# -> Int#
340 id2 = $$repPolyId
341
342 We implement this skip by inspecting the TH stage in `hasFixedRuntimeRep`.
343
344 A better solution would be to use 'CodeC' constraints, as in the paper
345 "Staging With Class", POPL 2022
346 by Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, Meng Wang
347 but for the moment, as we will typecheck again when splicing,
348 this shouldn't cause any problems in practice. See ticket #18170.
349
350 Test case: rep-poly/T18170a.
351
352 Note [Solving Concrete# constraints]
353 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
354 The representation polymorphism checks emit 'Concrete# ty' constraints,
355 as explained in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
356
357 The main mechanism through which a `Concrete# ty` constraint is solved
358 is to directly inspect 'ty' to check that it is a concrete type
359 such as 'TYPE IntRep' or `TYPE (TupleRep '[ TupleRep '[], FloatRep ])`,
360 and not, e.g., a skolem type variable.
361
362 There are, however, some interactions to take into account:
363
364 1. Decomposition.
365
366 The solving of `Concrete#` constraints works recursively.
367 For example, to solve a Wanted `Concrete# (TYPE r)` constraint,
368 we decompose it, emitting a new `Concrete# @RuntimeRep r` Wanted constraint,
369 and use it to solve the original `Concrete# (TYPE r)` constraint.
370 This happens in the canonicaliser -- see GHC.Tc.Solver.Canonical.canDecomposableConcretePrim.
371
372 Note that Decomposition fully solves `Concrete# ty` whenever `ty` is a
373 concrete type. For example:
374
375 Concrete# (TYPE (BoxedRep Lifted))
376 ==> (decompose)
377 Concrete# (BoxedRep Lifted)
378 ==> (decompose)
379 Concrete# Lifted
380 ==> (decompose)
381 <nothing, since Lifted is nullary>
382
383 2. Rewriting.
384
385 In PHASE 1 (as per Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete),
386 we don't have to worry about a 'Concrete#' constraint being rewritten.
387 We only need to zonk: if e.g. a metavariable, `alpha`, gets unified with `IntRep`,
388 we should be able to solve `Concrete# alpha`.
389
390 In PHASE 2, we will need to proceed as in GHC.Tc.Solver.Canonical.canClass:
391 if we have a constraint `Concrete# (F ty1)` and a coercion witnessing the reduction of
392 `F`, say `co :: F ty1 ~# ty2`, then we will solve `Concrete# (F ty1)` in terms of `Concrete# ty2`,
393 by rewriting the evidence for `Concrete# ty2` using `co` (see GHC.Tc.Solver.Canonical.rewriteEvidence).
394
395 3. Backpack
396
397 Abstract 'TyCon's in Backpack signature files are always considered to be concrete.
398 This is because of the strong restrictions around how abstract types are allowed
399 to be implemented, as laid out in Note [Synonyms implement abstract data] in GHC.Tc.Module.
400 In particular, no variables or type family applications are allowed.
401
402 Examples: backpack/should_run/T13955.bkp, rep-poly/RepPolyBackpack2.
403 -}
404
405 -- | A coercion hole used to store evidence for `Concrete#` constraints.
406 --
407 -- See Note [The Concrete mechanism].
408 type ConcreteHole = CoercionHole
409
410 -- | Evidence for a `Concrete#` constraint:
411 -- essentially a 'ConcreteHole' (a coercion hole) that will be filled later,
412 -- except:
413 --
414 -- - we might already have the evidence now; no point in creating a coercion hole
415 -- in that case;
416 -- - we sometimes skip the check entirely, e.g. in Typed Template Haskell
417 -- (see [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]).
418 data ConcreteEvidence
419 = ConcreteReflEvidence
420 -- ^ We have evidence right now: don't bother creating a 'ConcreteHole'.
421 | ConcreteTypedTHNoEvidence
422 -- ^ We don't emit 'Concrete#' constraints in Typed Template Haskell.
423 -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep].
424 | ConcreteHoleEvidence ConcreteHole
425 -- ^ The general form of evidence: a 'ConcreteHole' that should be
426 -- filled in later by the constraint solver, as per
427 -- Note [Solving Concrete# constraints].
428
429 -- | Check that the kind of the provided type is of the form
430 -- @TYPE rep@ for a __fixed__ 'RuntimeRep' @rep@.
431 --
432 -- If this isn't immediately obvious, for instance if the 'RuntimeRep'
433 -- is hidden under a type-family application such as
434 --
435 -- > ty :: TYPE (F x)
436 --
437 -- this function will emit a new Wanted 'Concrete#' constraint.
438 hasFixedRuntimeRep :: FRROrigin -> Type -> TcM ConcreteEvidence
439 hasFixedRuntimeRep frrOrig ty
440
441 -- Shortcut: check for 'Type' and 'UnliftedType' type synonyms.
442 | TyConApp tc [] <- ki
443 , tc == liftedTypeKindTyCon || tc == unliftedTypeKindTyCon
444 = return ConcreteReflEvidence
445
446 | otherwise
447 = do { th_stage <- getStage
448 ; if
449 -- We have evidence for 'Concrete# ty' right now:
450 -- no need to emit a constraint/create an evidence hole.
451 | isConcrete ki
452 -> return ConcreteReflEvidence
453
454 -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep].
455 | Brack _ (TcPending {}) <- th_stage
456 -> return ConcreteTypedTHNoEvidence
457
458 -- Create a new Wanted 'Concrete#' constraint and emit it.
459 | otherwise
460 -> do { loc <- getCtLocM (FixedRuntimeRepOrigin ty frrOrig) (Just KindLevel)
461 ; (hole, ct_ev) <- newConcretePrimWanted loc ki
462 ; emitSimple $ mkNonCanonical ct_ev
463 ; return $ ConcreteHoleEvidence hole } }
464 where
465 ki :: Kind
466 ki = typeKind ty
467
468 -- | Create a new (initially unfilled) coercion hole,
469 -- to hold evidence for a @'Concrete#' (ty :: ki)@ constraint.
470 newConcreteHole :: Kind -- ^ Kind of the thing we want to ensure is concrete (e.g. 'runtimeRepTy')
471 -> Type -- ^ Thing we want to ensure is concrete (e.g. some 'RuntimeRep')
472 -> TcM ConcreteHole
473 newConcreteHole ki ty
474 = do { concrete_ty <- newFlexiTyVarTy ki
475 ; let co_ty = mkHeteroPrimEqPred ki ki ty concrete_ty
476 ; newCoercionHole co_ty }
477
478 -- | Create a new 'Concrete#' constraint.
479 newConcretePrimWanted :: CtLoc -> Type -> TcM (ConcreteHole, CtEvidence)
480 newConcretePrimWanted loc ty
481 = do { let
482 ki :: Kind
483 ki = typeKind ty
484 ; hole <- newConcreteHole ki ty
485 ; let
486 wantedCtEv :: CtEvidence
487 wantedCtEv =
488 CtWanted
489 { ctev_dest = HoleDest hole
490 , ctev_pred = mkTyConApp concretePrimTyCon [ki, ty]
491 , ctev_nosh = WOnly -- WOnly, because Derived Concrete# constraints
492 -- aren't useful: solving a Concrete# constraint
493 -- can't cause any unification to take place.
494 , ctev_loc = loc
495 }
496 ; return (hole, wantedCtEv) }
497
498 {-***********************************************************************
499 * *
500 HsWrapper
501 * *
502 ***********************************************************************-}
503
504 -- | Smart constructor to create a 'WpFun' 'HsWrapper'.
505 --
506 -- Might emit a 'Concrete#' constraint, to check for
507 -- representation polymorphism. This is necessary, as 'WpFun' will desugar to
508 -- a lambda abstraction, whose binder must have a fixed runtime representation.
509 mkWpFun :: HsWrapper -> HsWrapper
510 -> Scaled TcType -- ^ the "from" type of the first wrapper
511 -> TcType -- ^ either type of the second wrapper (used only when the
512 -- second wrapper is the identity)
513 -> WpFunOrigin -- ^ what caused you to want a WpFun?
514 -> TcM HsWrapper
515 mkWpFun WpHole WpHole _ _ _ = return $ WpHole
516 mkWpFun WpHole (WpCast co2) (Scaled w t1) _ _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcRepReflCo t1) co2)
517 mkWpFun (WpCast co1) WpHole (Scaled w _) t2 _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) (mkTcRepReflCo t2))
518 mkWpFun (WpCast co1) (WpCast co2) (Scaled w _) _ _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) co2)
519 mkWpFun co1 co2 t1 _ wpFunOrig
520 = do { _concrete_ev <- hasFixedRuntimeRep (FRRWpFun wpFunOrig) (scaledThing t1)
521 ; return $ WpFun co1 co2 t1 }