Skip to content

Check for representation polymorphism in the typechecker using Concrete#

sheaf requested to merge sheaf/ghc:runtime-reps into master

This patch moves the representation polymorphism checks from the desugarer to the typechecker, by introducing a magic Concrete# predicate, and emitting Concrete# Wanted constraints to rule out representation polymorphism where it isn't allowed. A broad outline in laid out in the wiki page FixedRuntimeRep.

This only implements phase 1 of the plan outlined on the wiki page: we don't allow Concrete# constraints to be rewritten (only zonked), so this doesn't add support for type families in RuntimeReps.

Fixes these tickets:

The tickets concerning type families (such as #13105) are left as future work. See also the tickets tagged with representation polymorphism.

Here's a list of the representation polymorphism checks that I have come across which already exist in the compiler; I'm tracking which of these have been handled with the Concrete# mechanism.

  • In expressions:

    • Applications: GHC.Tc.Gen.App.tcEValArg, test T12973
    • Bindings: GHC.Tc.Gen.Binds.tcPolyBinds, test LevPolyLet
    • Ids: GHC.Tc.Gen.App.tcApp, tests T17817 and RepPolyWrappedVar
    • Record update: GHC.Tc.Gen.tcRecordField, test RepPolyRecordUpdate
    • Tuple constructors (boxed and unboxed): GHC.Tc.Gen.tcTupArgs, tests RepPolyTuple and RepPolyTupleSection
    • Unboxed sum constructors: GHC.Tc.Gen.tcExpr (ExplicitSum), test RepPolySum
    • Static pointers: no special check needed.
    • Explicit lists: no special check needed (these are never rebindable syntax).
    • Arithmetic sequences: no special check needed (enumFrom/enumFromTo/... aren't rebindable).
    • List comprehensions: no special checks needed (no rebindable syntax).
    • Do notation: GHC.Tc.Gen.Match.tcDoStmt, tests RepPolyDoBind, RepPolyDoBody1, RepPolyDoBody2, RepPolyDoReturn.
    • Monad comprehensions: similar treatment as do notation, but in GHC.Tc.Gen.Match.tcMcStmt. Tests RepPolyMcBody, RepPolyMcBind, RepPolyMcGuard.
    • TransformListComp: using must have a type of the form (a -> b) -> [a] -> [[a]], even with RebindableSyntax and OverloadedLists enabled. This means no check is needed.
    • Various arrow expressions: the arrow syntax functions are handled in GHC.Tc.Utils.Instantiate.tcSyntaxName, with other checks peppered throughout GHC.Tc.Gen.Arrow. It's been quite difficult to write tests which actually run into these checks, but I've added RepPolyArrowFun and RepPolyArrowCmd. The error messages are substantially improved: the old errors would print internal names like ds_d1D0 instead of the actual syntax name (e.g. arr or first).
    • dsHsWrapper: handled in mkWpFun (not sure which module to put mkWpFun in right now).
    • dsSyntaxExpr: I think I don't want to insert checks here, although it is easily doable.
  • In patterns

    • Variable patterns: GHC.Tc.Gen.Pat.tc_pat, test RepPolyBinder
    • Wildcard patterns: GHC.Tc.Gen.Pat.tc_pat, test RepPolyWildcardPattern
    • n+k patterns: GHC.Tc.Gen.Pat.tc_pat, test RepPolyNPlusK
    • Unboxed tuple patterns: GHC.Tc.Gen.Pat.tc_pat, test RepPolyUnboxedPatterns
    • PatBind: the other checks are sufficient. Test RepPolyPatBind.
    • selectConMatchVars: the other checks are sufficient.
    • matchWrapper: GHC.Tc.Gen.Match.tcMatches, test RepPolyMatch.
    • CoPat: no special check needed, as the other checks in patterns prevent representation-polymorphism from sneaking through.
  • In types

    • Typeclass method types: the check in GHC.Tc.TyCl.checkValidClass seems to be redundant, as representation polymorphism should already be prevented by GHC.Tc.Gen.TyCl.tcClassSigType
    • Data constructor declarations: the existing check in GHC.Tc.TyCl.checkValidDataCon is fine
    • Pattern synonym declarations: the existing check in GHC.Tc.Gen.Sig.tcPatSynSig covers arguments, and needs to be augmented with a check for the scrutinee type. Tests: RepPolyPatSynArg, RepPolyPatSynRes.
    • RULES: these caused a few issues, until I realised that we must never quantify over FixedRuntimeRep constraints in RULES (and also because of a bug that Richard introduced in GHC.Tc.Utils.TcMType.cloneWanted).

Further items:

  • Investigate performance regressions in T12545, T14683, T16577, T5631, T5642: the regressions seemed to be largely due to extra zonking that was needed with FixedRuntimeRep# checks; these zonks are no longer needed with Concrete#.
  • Adjust the mechanism to avoid requiring that the kind of the type being checked must immediately be of the form TYPE rep, allow this observation to be deferred.
  • Ensure that Ed Kmett's unboxed library can be compiled (provided one adds some Concrete instances in signature files to satisfy the representation-polymorphism checker).
  • Don't allow FixedRuntimeRep constraints to be deferred: test RepPolyDeferred.
  • Emit a custom error message when FixedRuntimeRep constraints go unsolved, instead of "No instance for FixedRuntimeRep rep".
  • Don't allow user-written FixedRuntimeRep Givens (tests UserFRR{1,2,3,4}).
  • Allow user-written FixedRuntimeRep instances in backpack signature files, same as for KnownNat, Coercible etc
  • Remove the checks in the desugarer & zonker that are rendered obsolete.
  • Remove the dsWhenNoErrs mechanism.
  • Write Note [The FixedRuntimeRep mechanism] in GHC.Tc.Instance.Class to briefly explain how FixedRuntimeRep works.
  • Update Note [Representation polymorphism checking] in GHC.HsToCore.Monad: rewritten and moved to GHC.Tc.Types.Origin to go above FRROrigin.
  • Update Note [Checking for representation-polymorphic functions]: rewritten and moved to GHC.Tc.Gen.App where the check now happens.
  • Update Note [Representation-polymorphic Ids] in GHC.Types.Id: deleted the note, as it is now subsumed by Note [Checking for representation-polymorphic functions].
  • Update Note [Desugaring representation-polymorphic applications] in GHC.HsToCore.Utils: deleted, as all of that complexity is now gone.
  • Update defer_type_errors.rst
  • Update the GHC 9.4 release notes.
Edited by sheaf

Merge request reports