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 simonpj

Keywords: TypeFamilies added

comment:2 Changed 9 months ago by adamgundry

Cc: adamgundry added

comment:3 Changed 9 months ago by diatchki

Cc: diatchki added

comment:4 Changed 9 months ago by gridaphobe

Cc: gridaphobe added

comment:5 Changed 9 months ago by bravit

Cc: bravit added

comment:6 in reply to:  description ; Changed 9 months ago by AntC

Replying to simonpj:

... quite a bit shorter.

To be clear what's intended here: the "shorter" could be achieved by something akin to Common Subexpression Elimination. That is:

  • Common type (sub-)expressions appearing in constaints.
  • Replace by a bare unification tyvar.
  • Add a ~ constraint between the tyvar and the type expression.

But wait, there's more:

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).

The ~ constraint generated for the common type expression FieldType is exactly the superclass constraint for HasField, just as Eq 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 a HasField instance -- because FieldType 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.

There is nothing record-specific about this ticket. It's just about using inferred equality constraints to simplify the inferred signature.

comment:7 in reply to:  6 Changed 9 months ago by gridaphobe

Replying to AntC:

Note also a later comment on that github discussion that the FieldType constraint holding implies there's a HasField instance -- because FieldType 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 simonpj

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), where t2 = ty[t1/a,t3/c], then replace all occurrences of t2 in preds with x 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 the Description.

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.

Note: See TracTickets for help on using tickets.