Skip to content
  • sheaf's avatar
    b27b2af3
    Introduce ConcreteTv metavariables · b27b2af3
    sheaf authored and Marge Bot's avatar Marge Bot committed
      This patch introduces a new kind of metavariable, by adding the
      constructor `ConcreteTv` to `MetaInfo`. A metavariable with
      `ConcreteTv` `MetaInfo`, henceforth a concrete metavariable, can only
      be unified with a type that is concrete (that is, a type that answers
      `True` to `GHC.Core.Type.isConcrete`).
    
      This solves the problem of dangling metavariables in `Concrete#`
      constraints: instead of emitting `Concrete# ty`, which contains a
      secret existential metavariable, we simply emit a primitive equality
      constraint `ty ~# concrete_tv` where `concrete_tv` is a fresh concrete
      metavariable.
    
      This means we can avoid all the complexity of canonicalising
      `Concrete#` constraints, as we can just re-use the existing machinery
      for `~#`.
    
      To finish things up, this patch then removes the `Concrete#` special
      predicate, and instead introduces the special predicate `IsRefl#`
      which enforces that a coercion is reflexive.
      Such a constraint is needed because the canonicaliser is quite happy
      to rewrite an equality constraint such as `ty ~# concrete_tv`, but
      such a rewriting is not handled by the rest of the compiler currently,
      as we need to make use of the resulting coercion, as outlined in the
      FixedRuntimeRep plan.
    
      The big upside of this approach (on top of simplifying the code)
      is that we can now selectively implement PHASE 2 of FixedRuntimeRep,
      by changing individual calls of `hasFixedRuntimeRep_MustBeRefl` to
      `hasFixedRuntimeRep` and making use of the obtained coercion.
    b27b2af3
    Introduce ConcreteTv metavariables
    sheaf authored and Marge Bot's avatar Marge Bot committed
      This patch introduces a new kind of metavariable, by adding the
      constructor `ConcreteTv` to `MetaInfo`. A metavariable with
      `ConcreteTv` `MetaInfo`, henceforth a concrete metavariable, can only
      be unified with a type that is concrete (that is, a type that answers
      `True` to `GHC.Core.Type.isConcrete`).
    
      This solves the problem of dangling metavariables in `Concrete#`
      constraints: instead of emitting `Concrete# ty`, which contains a
      secret existential metavariable, we simply emit a primitive equality
      constraint `ty ~# concrete_tv` where `concrete_tv` is a fresh concrete
      metavariable.
    
      This means we can avoid all the complexity of canonicalising
      `Concrete#` constraints, as we can just re-use the existing machinery
      for `~#`.
    
      To finish things up, this patch then removes the `Concrete#` special
      predicate, and instead introduces the special predicate `IsRefl#`
      which enforces that a coercion is reflexive.
      Such a constraint is needed because the canonicaliser is quite happy
      to rewrite an equality constraint such as `ty ~# concrete_tv`, but
      such a rewriting is not handled by the rest of the compiler currently,
      as we need to make use of the resulting coercion, as outlined in the
      FixedRuntimeRep plan.
    
      The big upside of this approach (on top of simplifying the code)
      is that we can now selectively implement PHASE 2 of FixedRuntimeRep,
      by changing individual calls of `hasFixedRuntimeRep_MustBeRefl` to
      `hasFixedRuntimeRep` and making use of the obtained coercion.
Loading