Separate Constraint from Type in Core.
Needs RevisionPublic

Authored by goldfire on Jan 25 2017, 10:37 PM.

Details

Summary

See comment:47 on Trac #11715. It turned out that there was no
need to worry about unwrapping newtypes.

But there is a problem: how do we reject types like
Eq a -> a -> a? Note that I've written -> instead of
=>! Now, Eq a, having kind TYPE blah, is a perfectly
good argument to ->. Because we need to allow for unification,
we can't really sort this out until we zonk. But by then, the
HsSyn is long gone, so we can't figure out that the user
swapped the arrows.

Test Plan

./validate

goldfire retitled this revision from to Separate Constraint from Type in Core..Jan 25 2017, 10:37 PM
goldfire updated this object.
goldfire edited the test plan for this revision. (Show Details)
goldfire added reviewers: simonpj, bgamari, austin.
goldfire updated the Trac tickets for this revision.

But there is a problem: how do we reject types like

Eq a -> a -> a?

Interestingly, the proposal of having a coherency flag on TYPE would solve this. A (->) arrow would get expected kind TYPE Incoherent r0, where r0 is a unification variable.

That's an interesting strike in its favour.

In thinking about this, I think adding the Coherency argument to TYPE might be the only solution. As it stands we're in a strange space: If I have forall (r :: RuntimeRep) (a :: TYPE r). a -> a, then any choice of r is OK except ConstraintRep -- because ConstraintRep requires a => (and can't be returned from a function, besides). This bump in the surface tells me we have the wrong design. The "obvious" way forward is to add another parameter to TYPE. Then it's all easy. And tuples can be made to infer their kind more naturally.

Having another parameter to TYPE also solves another small wrinkle in this patch. The noinline function is used in interface files to provide loop-breakers when hs-boot files are involved. See Note [Inlining and hs-boot files] in ToIface. However, we sometimes need to apply noinline to dictionaries. If Constraint /= Type, then noinline needs to be levity polymorphic. Except that it really shouldn't be -- it should be coherency-polymorphic. Note also that coherency doesn't affect the code generator at all, so I could define

noinline :: forall (c :: Coherency) (a :: TYPE c LiftedRep). a -> a
noinline x = x

and no one will complain. Well, the type checker will complain because we potentially have constraints where we shouldn't, but it's much easier to let the type-checker allow this magical definition to be accepted than to deal with the full levity-polymorphic version.

bgamari requested changes to this revision.Feb 2 2017, 12:11 PM

Bumping out of review queue as we decided to punt this to 8.4.

This revision now requires changes to proceed.Feb 2 2017, 12:11 PM
austin resigned from this revision.Nov 9 2017, 11:32 AM