Check for representation polymorphism in the typechecker using Concrete#
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 RuntimeRep
s.
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
, testT12973
-
Bindings: GHC.Tc.Gen.Binds.tcPolyBinds
, testLevPolyLet
-
Id
s:GHC.Tc.Gen.App.tcApp
, testsT17817
andRepPolyWrappedVar
-
Record update: GHC.Tc.Gen.tcRecordField
, testRepPolyRecordUpdate
-
Tuple constructors (boxed and unboxed): GHC.Tc.Gen.tcTupArgs
, testsRepPolyTuple
andRepPolyTupleSection
-
Unboxed sum constructors: GHC.Tc.Gen.tcExpr
(ExplicitSum
), testRepPolySum
-
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
, testsRepPolyDoBind
,RepPolyDoBody1
,RepPolyDoBody2
,RepPolyDoReturn
. -
Monad comprehensions: similar treatment as do notation, but in GHC.Tc.Gen.Match.tcMcStmt
. TestsRepPolyMcBody
,RepPolyMcBind
,RepPolyMcGuard
. -
TransformListComp
:using
must have a type of the form(a -> b) -> [a] -> [[a]]
, even withRebindableSyntax
andOverloadedLists
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 throughoutGHC.Tc.Gen.Arrow
. It's been quite difficult to write tests which actually run into these checks, but I've addedRepPolyArrowFun
andRepPolyArrowCmd
. The error messages are substantially improved: the old errors would print internal names likeds_d1D0
instead of the actual syntax name (e.g.arr
orfirst
). -
dsHsWrapper
: handled inmkWpFun
(not sure which module to putmkWpFun
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
, testRepPolyBinder
-
Wildcard patterns: GHC.Tc.Gen.Pat.tc_pat
, testRepPolyWildcardPattern
-
n+k patterns: GHC.Tc.Gen.Pat.tc_pat
, testRepPolyNPlusK
-
Unboxed tuple patterns: GHC.Tc.Gen.Pat.tc_pat
, testRepPolyUnboxedPatterns
-
PatBind
: the other checks are sufficient. TestRepPolyPatBind
. -
selectConMatchVars
: the other checks are sufficient. -
matchWrapper
:GHC.Tc.Gen.Match.tcMatches
, testRepPolyMatch
. -
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 byGHC.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 inGHC.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 withConcrete#
. -
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 someConcrete
instances in signature files to satisfy the representation-polymorphism checker). -
Don't allow FixedRuntimeRep
constraints to be deferred: testRepPolyDeferred
. -
Emit a custom error message when FixedRuntimeRep
constraints go unsolved, instead of "No instance for FixedRuntimeRep rep". -
Don't allow user-written FixedRuntimeRep
Givens (testsUserFRR{1,2,3,4}
). -
Allow user-written FixedRuntimeRep
instances in backpack signature files, same as forKnownNat
,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 howFixedRuntimeRep
works. -
Update Note [Representation polymorphism checking] in GHC.HsToCore.Monad
: rewritten and moved toGHC.Tc.Types.Origin
to go aboveFRROrigin
. -
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.