Opened 9 months ago
Last modified 9 months ago
#16070 new bug
Better inferred signatures
Reported by: | simonpj | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.6.3 |
Keywords: | TypeFamilies | Cc: | adamgundry, diatchki, gridaphobe, bravit |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
Consider this (taken from here)
class FieldType x r ~ a => HasField (x :: k) r a where type FieldType x r getField :: r -> a setField :: r -> a -> r f r = setField @"bar" r (getField @"foo" r)
We get this type inferred for f
:
f :: forall r. (HasField "bar" r (FieldType "bar" r), HasField "foo" r (FieldType "bar" r)) => r -> r
But actually this signature is equivalent
f :: forall r a. (HasField "bar" r a, HasField "foo" r a) => r -> r
and it's quite a bit shorter. Similarly, from this definition
g r = setField r
We get this inferred type
g :: forall r p. HasField "bar" r (FieldType "bar" r) => p -> r -> FieldType "bar" r -> r
where again we might prefer
g :: forall r a. HasField "bar" r a => r -> a -> r
Question: could we make GHC infer the briefer types?
After all, it does some similar abbreviation with type classes. Where we could
infer (Ord a, Eq a)
we collapse out the Eq a
and just infer the context
(Ord a)
.
There is nothing record-specific about this ticket. It's just about using inferred equality constraints to simplify the inferred signature.
Change History (8)
comment:1 Changed 9 months ago by
Keywords: | TypeFamilies added |
---|
comment:2 Changed 9 months ago by
Cc: | adamgundry added |
---|
comment:3 Changed 9 months ago by
Cc: | diatchki added |
---|
comment:4 Changed 9 months ago by
Cc: | gridaphobe added |
---|
comment:5 Changed 9 months ago by
Cc: | bravit added |
---|
comment:6 follow-up: 7 Changed 9 months ago by
comment:7 Changed 9 months ago by
Replying to AntC:
Note also a later comment on that github discussion that the
FieldType
constraint holding implies there's aHasField
instance -- becauseFieldType
is an Associated Type. Using that implication seems harder: Assoc Types are treated as sugar for top-level type families/not necessarily grounded in instances, which already gives trouble.
I was also concerned about this, in particular what happens if we have a type instance
for an associated type at the top-level? But it turns out that GHC does not allow that, all instances of associated types must be defined in the context of a class instance. So I think using the FieldType => HasField
implication could work nicely.
comment:8 Changed 9 months ago by
Yes, I was thinking of the following algorithm. The algorithm is used when inferring the type of a function (and only on that occasion). Specifically, it is an enhancement to the existing function TcType.mkMinimalBySCs
.
Suppose C
is declared thus, with a type variable on the left of a superclass equality:
class (b ~ ty, ...) => C a b c
mkMinimalBySCs
is given a list of predicates, preds
, such as (Ord a, Eq a)
, or (HasField "foo" r (FieldType "foo" r))
.
It's business is to abbreviate it to an equivalent one.
- For each predicate
(C t1 t2 t3)
, wheret2
=ty[t1/a,t3/c]
, then replace all occurrences oft2
inpreds
withx
where is a fresh skolem variable.
So if
preds = [ HasField "bar" r (FieldType "bar" r) , HasField "foo" r (FieldType "bar" r) ]
we'll spot the condition on the first predicate, and replace (FieldType "bar" r)
with x
throughout:
preds = [ HasField "bar" r x , HasField "foo" r x ]
Now we need to
- Quantify over
x
as well as whatever else we were quantifying over before - Apply that same substitution to the type we are quantifying over (to catch the case of
g
in theDescription
.
So it's more than just modifyign mkMinimalBySCs
.
There's something a bit unsatisfying about this: during flattening we have all these common sub-expressions neatly identified. It seems a pity to un-flatten them away only to then have to rediscover them.
Replying to simonpj:
To be clear what's intended here: the "shorter" could be achieved by something akin to Common Subexpression Elimination. That is:
~
constraint between the tyvar and the type expression.But wait, there's more:
The
~
constraint generated for the common type expressionFieldType
is exactly the superclass constraint forHasField
, just asEq a
is a superclass constraint for(Ord a)
.Note also a later comment on that github discussion that the
FieldType
constraint holding implies there's aHasField
instance -- becauseFieldType
is an Associated Type. Using that implication seems harder: Assoc Types are trreated as sugar for top-level type families/not necessarily grounded in instances, which already gives trouble.