[GHC] #16070: Better inferred signatures
#16070: Better inferred signatures -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider this (taken from [https://github.com/ghc-proposals/ghc- proposals/pull/158#issuecomment-448549030 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16070 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16070: Better inferred signatures -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeFamilies -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16070#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16070: Better inferred signatures -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16070#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16070: Better inferred signatures -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by diatchki): * cc: diatchki (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16070#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16070: Better inferred signatures -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by gridaphobe): * cc: gridaphobe (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16070#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16070: Better inferred signatures -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bravit): * cc: bravit (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16070#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16070: Better inferred signatures -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [ticket:16070 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16070#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16070: Better inferred signatures -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by gridaphobe): Replying to [comment:6 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16070#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16070: Better inferred signatures -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16070#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC