Opened 5 months ago
Last modified 3 months 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 )
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 5 months ago by
Summary: | Should accept a type that needs coercion quantification → Should GHC accept a type signature that needs coercion quantification? |
---|
comment:2 Changed 5 months ago by
comment:3 Changed 5 months ago by
Keywords: | TypeInType added |
---|
comment:4 Changed 5 months ago by
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.
comment:5 Changed 4 months ago by
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 4 months ago by
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 4 months ago by
Description: | modified (diff) |
---|
comment:8 Changed 4 months ago by
When we get this, we can remove Note [Emitting the residual implication in simplifyInfer]
in TcSimplify. See comment:5:ticket:15497.
comment:9 Changed 4 months ago by
Related Tickets: | → #12677 |
---|
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., writeDict (a ~ b)
, whereDict :: 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.
CONSTRAINT :: RuntimeRep -> Type
.Constraint
becomes a synonym forCONSTRAINT LiftedRep
.Constraint
.~
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 traditionalDict
won't work here, but any user could define aDict#
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.)