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 }