Note [hasFixedRuntimeRep]
The 'hasFixedRuntimeRep' function is responsible for taking a type 'ty' and emitting a constraint to ensure that 'ty' has a fixed `RuntimeRep`, as outlined in Note [The Concrete mechanism]. To do so, we compute the kind 'ki' of 'ty', create a new concrete metavariable `concrete_tv` of kind `ki`, and emit a constraint `ki ~# concrete_tv`, which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRep. If we can solve the equality constraint, i.e. produce a coercion `kco :: ki ~# concrete_tv`, then 'hasFixedRuntimeRep' returns the coercion co = GRefl ty kco :: ty ~# ty |> kco The RHS of the coercion `co` is `ty |> kco`. The kind of this type is concrete (by construction), which means that `ty |> kco` is an FRRType in the sense of Note [Fixed RuntimeRep], so that we can directely compute its runtime representation using `typePrimRep`. [Wrinkle: Typed Template Haskell] We don't perform any checks when type-checking a typed Template Haskell quote: we want to allow representation polymorphic quotes, as long as they are monomorphised at splice site. Example: Module1 repPolyId :: forall r (a :: TYPE r). CodeQ (a -> a) repPolyId = [|| \ x -> x ||] Module2 import Module1 id1 :: Int -> Int id1 = $$repPolyId id2 :: Int# -> Int# id2 = $$repPolyId We implement this skip by inspecting the TH stage in `hasFixedRuntimeRep`. A better solution would be to use 'CodeC' constraints, as in the paper "Staging With Class", POPL 2022 by Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, Meng Wang but for the moment, as we will typecheck again when splicing, this shouldn't cause any problems in practice. See ticket #18170. Test case: rep-poly/T18170a.
References 2
- Fixed RuntimeRep GHC.Tc.Utils.Concrete
- The Concrete mechanism GHC.Tc.Utils.Concrete
Referenced by 8
- GHC.Tc.Utils.TcMType call site ×4
- GHC.Tc.Gen.App call site
- GHC.Tc.Types.Evidence call site
- Concrete overview GHC.Tc.Utils.Concrete
- GHC.Tc.Utils.Concrete call site