Opened 2 months ago

Last modified 6 weeks ago

#15710 new bug

Should GHC accept a type signature that needs coercion quantification?

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #12677 Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

Consider

f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x
f = error "uk"

Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being

f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1->*)). (f |> co) x

But there is a problem: the user wrote k ~ (k1 -> *), and that's a boxed value that we can't take apart in types. I'm not sure what to do here.

These thoughts arose when contemplating Note [Emitting the residual implication in simplifyInfer] in TcSimplify; see comment:5 in #15497

Change History (10)

comment:1 Changed 2 months ago by simonpj

Summary: Should accept a type that needs coercion quantificationShould GHC accept a type signature that needs coercion quantification?

comment:2 Changed 2 months ago by goldfire

Back when I was implementing -XTypeInType, your "problem" at the end was indeed a problem. There are some notes (meant mainly for myself) here.

Briefly, the problem was: how should we interpret a user-written ~? Should it be a lifted/boxed thing or an unlifted/unboxed thing? If it's lifted, then we can abstract over it (e.g., write Dict (a ~ b), where Dict :: Constraint -> Type). If it's unlifted, we can write the program in the original ticket.

However, we now have a robust levity polymorphism mechanism, meaning that we can now abstract over unlifted things quite handily. There has also been recent musing about strict constraints, which fits in nicely. So, here's a sketch for how to do this.

  1. Introduce CONSTRAINT :: RuntimeRep -> Type. Constraint becomes a synonym for CONSTRAINT LiftedRep.
  1. Existing constraints would continue to have kind Constraint.
  1. Give ~ this new kind: (~) :: forall k. k -> k -> CONSTRAINT (TupleRep '[]) -- essentially saying that ~ is strict and erases to 0 bits.

Really, what I've done here is made the user-facing equality ~ the same as the internal equality ~#. (This will make even more sense when ~# is homogeneous, like ~ is.)

One might wonder about deferred type errors. I claim that this is a red herring. Since GHC 8.0, GHC has been strict in equality errors anyway. This is described in #11197. The solution is conceptually simple (but no one has implemented it yet): aggressively float-in case-matches on deferred type errors.

One might also wonder about Dict (a ~ b) in this brave new world. It's true that the traditional Dict won't work here, but any user could define a Dict# that would, by abstracting over erased, strict constraints. Perhaps this change would be breaking enough that we'd need to keep ~ lifted and introduce a new name for the unlifted equality that could be used in coercion quantification, but I think we can debate that problem separately from the general design. (Note that it's very easy for a user to introduce a lifted equality type that wraps the unlifted one.)

comment:3 Changed 2 months ago by goldfire

Keywords: TypeInType added

comment:4 Changed 2 months ago by simonpj

In #15648 you argued that (t1 ~# t2) should not be a constraint, should not return True to isPredTy, and should not be an invisible parameter, implicitly instantiated at call sites.

Here you seem to be arguing the exact opposite!

I'm uncomfortable with forcing the the user to deal with both (~) and (~#); I wanted the latter to be an implementation detail. Even putting it in a constraint tuple like f :: (Num a, a ~ b) => blah is problematic if a~b is unlifted/unboxed.

Our "all constraints are boxed" story was working perfectly well right up to this, when we add coercion quantification. But I don't see a way to reconcile it with coercion quantification. Alas.

Last edited 2 months ago by simonpj (previous) (diff)

comment:5 Changed 2 months ago by goldfire

Yes, I'm arguing both sides -- but with good reason. t1 ~# t2 is not a constraint today, and thus it shouldn't respond to isPredTy. But this ticket is all about tomorrow, when I do think it could become a constraint.

Would we be more efficient if constraints could be strict and unboxed? I imagine "yes". If so, then the current story isn't working as well as it could be.

As for tupling: we could make ( ... ) be an unboxed tuple if it's written to the left of =>. In the end, I just think of the parens and commas as concrete syntax for some unspecified abstract syntax that handles sets of constraints here. (This is not how I think of the argument to Dict, say, where order suddenly matters.)

comment:6 Changed 2 months ago by simonpj

Tupling: yes f :: (Num a, Ord a) => blah is already syntactic sugar for f :: Num a => Ord a => blah. But I'm more concerned about

type C a b = (Num a, a ~ b)

and here it'd be much trickier (and unprincipled) to switch to unboxed tuples. Moreover, we do lots of constraint abstraction

data Dict c where
  Dict :: c => Dict c

and we can't instantiate that polymorphic c with an unboxed tuple.

So yes, I think we could have Constraint and Constraint# just as we have Int and Int#. But it's very uncomfortable to have to use a ~# b in a type if (but only if) the constraint is used in a dependent way.

comment:7 Changed 2 months ago by simonpj

Description: modified (diff)

comment:8 Changed 2 months ago by goldfire

When we get this, we can remove Note [Emitting the residual implication in simplifyInfer] in TcSimplify. See comment:5:ticket:15497.

comment:9 Changed 2 months ago by RyanGlScott

comment:10 Changed 6 weeks ago by goldfire

#15870 is an example of someone actually trying this.

Note: See TracTickets for help on using tickets.