tweag / ghc

Fork of official GHC repository.

http://www.haskell.org/ghc/

Other

44 stars 5 forks source link

Use a predicate to check submultiplicity #506

Closed monoidal closed 4 years ago

monoidal commented 4 years ago

Currently, tcSubMult eagerly solves the constraint and works only when the evidence is a ReflCo. A cleaner way to enforce this condition is to have a predicate representing submultiplicity. This means we'll be able to get rid of WpMultCoercion, and show errors in the typechecker instead of desugarer. This has no user-visible effects except perhaps better error messages.

This is a well-defined issue, unlike more advanced ideas requiring research #390 #426. This will not fix test LinearPolyType. However, it might reduce the two "Multiplicity coercions not supported" messages to one.

As far as I understand, this is blocked on the PredTree refactoring.

aspiwack commented 4 years ago

I'm not sure this is different from #426 , really.

What is the PredTree refactoring?

monoidal commented 4 years ago

426 means exposing a constraint to the user, designing evidence for it and dealing with the case when it's a given (e.g. from p <= q, q <= r derive p <= r). In this ticket, we can keep the current algorithm, but report errors before desugaring.

The refactoring is https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2857.

aspiwack commented 4 years ago

Ah yes, I had indeed misunderstood #426 .

And I see. The point is that, currently, all predicate types must be types, hence have some kind of inhabitants as evidence. And it's a bit inconvenient for our use-case. I'm sure it would be possible to workaround the issue, so if this were to become urgent and the PredTree thing would not have made it in time; I'm sure this wouldn't be a blocker. But I see how it would be much more convenient if we have predicated independent from types.

monoidal commented 4 years ago

Moved to upstream:#18756.