[GHC] #16146: Trivial partial type signature kills type inference in the presence of GADTs
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | 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: -------------------------------------+------------------------------------- Suppose we have {{{#!hs data G a where G1 :: G Char G2 :: G Bool }}} If I now write {{{#!hs foo x = case x of G1 -> 'z' G2 -> True }}} I rightly get an error around untouchable variables. If I add the type signature {{{#!hs foo :: G a -> a }}} all is well again. So far, so good. Now, I write {{{#!hs foo :: forall a. G a -> a foo x = ((case x of G1 -> 'z' G2 -> True) :: _) }}} and I get those untouchable errors again. Untouchable-variable errors usually arise when there are multiple possible answers to the type inference problem. Yet, that isn't the case here: `_` must stand for `a`. Solution: mumble mumble bidirectional type inference mumble mumble. Part of the problem comes from Note [Partial expression signatures] in TcExpr, which states {{{ here is a guiding principile e :: ty should behave like let x :: ty x = e in x }}} Indeed, if we behave like that, the untouchable-variable errors are to be expected. But I also think that it would be a nice principle to say that `:: _` is always a no-op. This is not an idle nice-to-have: if we fix this, `singletons` will continue to work with GHC. Right now, it doesn't: https://github.com/goldfirere/singletons/issues/357 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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 RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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): It's not obvious what to do here. Consider {{{ f :: Int -> Int -> Int f x = (...blah...) :: forall a. a->a }}} Here the expression signature insists that `(..blah..)` has type `forall a. a->a` which is ''more general than'' the `Int -> Int` imposed by the signature for `f`. Now imagine a partial version of this: {{{ f :: Int -> Int -> Int f x = (...blah...) :: forall a. a -> _ }}} The same thing applies. Because the partial signature may be more general than the expected type from "outside", it's hard to take advantage of the latter until we've worked out what the fleshed-out partial signature is (ie. in this case perhaps `forall a. a->a`). Only then can we instantiate it to see if it is more general than `Int -> Int`. So while `(e :: _)` may be a no-op, that is not true of other partial type signatures. Short of making it a magic, ad-hoc special case, I'm not sure how to do better. Perhaps one could make a special case when the partial signature had no quantification. But it sounds smelly to me. Why not just remove the `:: _`? It's not doing anything useful. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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 goldfire): The real use case isn't `:: _` -- it's `:: Sing @_ (Something Big && Obnoxious)`. The right value for the `_` is being pushed down, but it can't be inferred from the expression in the signature. The signature is needed in some scenarios... not actually the one that's causing trouble, though. The problem is that I think it will be impossible for `singletons` to tell the difference between scenarios where it's needed and those where it isn't, so we need it not to interfere. The signature in question indeed does no quantification. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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): Well I suppose we could have a different typing rule for the case where there is no quantification. I'm not very keen on this, because it changes behaviour in a subtle way, and just adding an unrelated quantifier to the partial signature would completely change its typing rule. It's user-facing, so perhaps GHC-proposal-worthy? The relevant function is `tcExprSig`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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 goldfire): Why does quantification enter into it, now that I think of it? Let's look at some typing rules, where `<=` denotes checking and `=>` denotes inference in the bidirectional type system. I use `t` to denote a type (no wildcards) and `p` to denote a partial type (zero or more wildcards). {{{ e <= t ------------ Sig (e : t) => t e => t1 t1 <: t2 -------- Infer e <= t2 }}} These rules govern what happens when an expression with a complete type signature `(e : t1)` is checked against a type `t2`. Because there is no `<=` rule for the `(e : t1)` form, we use the Infer rule to switch into synthesis mode. Since we have `t1` as the type signature, we synthesize type `t1` for `(e : t1)`. Then, we check to make sure that `t1` is a subtype of `t2`. (Reminder: `t1` is a subtype of `t2` iff there is a computationally free way to convert a value of type `t1` to a value of type `t2`. Example: `forall a. a -> a` is a subtype of `Int -> Int` because we can instantiate a value of type `forall a. a -> a` with `Int` with no runtime cost.) Currently, this is the rule for an expression with a partial type signature: {{{ e <~~ p => t ------------ PartialSig (e : p) => t }}} where `e <~~ p => t` means that checking `e` against partial signature `p` results in a type `t`. This is done by GHC's `simplifyInfer`. I propose adding a new rule to the system: {{{ p <: t2 => p2 e <~~ p2 => t t <: t2 ------------- PartialSigCheck (e : p) <= t2 }}} where `p <: t2 => p2` means: 1. Check whether `p` is a subtype of `t2`. 2. During this check, we might have to choose values for wildcards in `p`. 3. `p2` is `p`, but with the wildcards zonked to have the values discovered in the subtype check. Note that `p2` might actually have no wildcards left. Regardless, we will use the `e <~~ p2 => t` (`simplifyInfer`) operation, as checking against a partial type signature is really quite different than checking against a complete type signature, and we wouldn't want unifications with the pushed-down type to chane this. Naturally, we have to do another subtype check, just to make sure that the type after `simplifyInfer` is suitable. (It's possible that we can prove that if `p <: t2 => p2` and `e <~~ p2 => t`, then `t <: t2`. Indeed, that would be desirable. But I'm not sure right now if this would be true.) I ''think'' that would solve our problem. And it seems to make GHC strictly more expressive. And it would seem to be "what the user would expect", making use of information manifestly available (but, today, ignored). This would require writing a new subtyping check `p <: t2 => p2`. The implementation of subtyping in GHC is somewhat laborious, but it's not a particularly complicated judgment. It's unclear how much code-sharing this new form would have with the existing one, given the different way that partial types are represented internally. I agree that this is a GHC proposal. However, the consequences of this are subtle and hard to predict, so I want to have some debate here before going there. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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): How do you propose to do step 1 (check that `p` is a subtype of `t2`)? Suppose `p` is `forall a. _ -> a`, and `t2` is `Int -> Int`. Now when we instantiate `p` (to do the subtype check), what do we do about that `_`?? We could satisfy the subtype with `_` = `Int`, or `_` = `a`. The point is that we can't hope to instantiate a partial type signature, and we should not attempt to do so. That's why I suggest that we might just squeeze by if there is visibly no quantification to be done. So I don't think comment:5 will work. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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 goldfire): Quite right in comment:6. We can't possibly instantiate a partial type. So then I got to thinking that we would check the ascribed expression first, followed by the subtype check (presumably after the partial type is no longer partial). But we should ''already'' be doing that. So I dived deeper, and I found more interesting things. We have, as before {{{#!hs data G a where G1 :: G Char G2 :: G Bool }}} I wish for this to be accepted: {{{#!hs foo :: forall a. G a -> a foo x = ((case x of G1 -> 'z' G2 -> True) :: _) }}} Why is it rejected today? It's not just that the wildcard is untouchable in the context of the GADT pattern-match. Here's what happens: we invent a new metavariable `_w` to stand for the wildcard. This `_w` is untouchable in the GADT pattern match, so we don't learn anything about it. Then, critically, we try to ''generalize'' the signature. This takes the unsolved metavariable `_w` and ''skolemizes'' it. So, later, when the subtype-checker tries to unify `_w` with the type variable `a`, it fails, as `_w` is a skolem. This behavior isn't entirely unreasonable. But note that I never asked for generalization. Contrast with the fact that (if I say `default ()`), GHC rejects {{{#!hs wurble :: _ wurble x = x + 1 }}} This is rejected because my partial type signature did not allow for any constraints (I need `Num a => a -> a`): GHC does not allow `_` to stand for `_ => _`. Yet GHC ''does'' allow `_` to stand for `forall a. a -> a`: changing `wurble` to be `wurble x = x` works just fine. This seems like inconsistent design, to me. So, I wonder if we should allow generalization in wildcards only by user request, with something like `forall _. _`, just like we do so currently for constraints. We could also have `forall a b c _ . ...`, just like we now can have an extra-constraints wildcard. (The `_` in `forall a b c _` isn't really a wildcard, but a request for generalization.) I'm not sure how implementable this is, but it's a decent thought experiment. Of course, the idea that "wildcards should not be generalized" reminded me of something else that should not be generalized: lets. And indeed we see some strange behavior around `let` and GADT inference. This isn't related to partial type signatures, but it's a bit more grist for the mill. Consider this: {{{#!hs bar :: G a -> a bar z = quux z where quux x = case x of G1 -> 'b' G2 -> True }}} This is rejected. `quux` is checked just like it were at top level, and we can't figure out its type. This is true even though bidirectional type- checking tells us that the type of `quux` should be `G a -> a`. However, earlier I argued that the problem is ''generalization''. So, let's suppress that urge of GHC's: {{{#!hs bar2 :: G a -> a bar2 z = quux2 z where quux2 x = case x of G1 -> const 'b' z G2 -> True }}} This is accepted! In the case-match for `G1`, I have an entirely- irrelevant use of the outer variable `z`. According to the rules for let- should-not-be-generalized, the appearance of a variable from an outer scope disables generalization. And so `quux2` is not generalized, meaning that its type still contains proper metavariables when we check that `quux2 z` has type `a`, and then GHC can infer the correct type. Relating back to partial type signatures, now we try {{{#!hs bar3 :: G a -> a bar3 z = quux3 z where quux3 :: _ quux3 x = case x of G1 -> const 'b' z G2 -> True }}} The only change here is the partial type signature. Because GHC does not respect let-should-not-be-generalized in the presence of partial type signatures, this is rejected again. Bottom line: it's nice to have finer control over generalization. The work on let-should-not-be-generalized supposed that a good heuristic for when to stop generalization was the presence of a variable from an outer scope. This has indeed served us well, and I don't propose changing it. But it might be nice to give users a way to control this behavior more directly. Having a partial type signature `xyz :: _` might be a signal saying not to generalize something that ordinarily would (helpful in my `quux` example) and having a partial type signature `xyz :: forall _. _` might a signal saying to generalize something that ordinarily wouldn't. This is useful: See Section 10.2 of my (as-yet-unpublished) [https://cs.brynmawr.edu/~rae/papers/2018/stitch/stitch.pdf Stitch paper]. (That section mentions 2 places where generalization is good. Interestingly, GHC has already adapted to the first point. The second point is of interest here, where I brutally just specified `-XNoMonoLocalBinds` in order to get generalization.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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 goldfire): Another interesting example has cropped up. Re-consider {{{#!hs wurble :: _ wurble x = x }}} This is accepted, because the type `_` allows for implicit generalization. But what about {{{#!hs wurble2 :: forall. _ wurble2 x = x }}} To my surprise, this is accepted too, with `wurble2 :: forall a. a -> a`. Yet, I would have expected my `forall.` to say that there are no quantified variables in the type of `wurble2`. So, maybe another design is this: `foo :: _` can be generalized. (This is at odds with the fact that `foo` cannot have constraints.) But if there is an explicit `forall` in type of `foo`, we appeal to the forall-or-nothing rule and say that the variables quantified in the `forall` are precisely the quantified variables; no more can be inferred. Then, we can suppress quantification in `forall. _`. One advantage here is that this new design is backward compatible (though I'm not terribly worried about that here). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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 goldfire): Also amongst all this was the observation that let-should-not-be- generalized is ignore in the presence of partial type signatures. Is this a good thing? I'm not sure. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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 goldfire): I'm pleased to report that we have singletons [https://github.com/goldfirere/singletons/issues/357#issuecomment-452935291 working again], but it will require users to write apparently-redundant type annotations in a few places. It would be nice to address this bug / design flaw so that singletons can become more ergonomic again. (Yes, I know this will have to go through the proposals process, but I still would like feedback here first.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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): '''Forall-or-nothing behaviour'''
Another interesting example has cropped up. Re-consider
Partial type signatures have always had the semantics that you can use a `forall` to bind the type variables you need to mention but the final type signature may have more. E.g. {{{ f :: forall a. _ -> a -> Bool f x y = True }}} Here the final sig is `f :: forall a b. b -> a -> Bool`. It would be possible to say that * If you use a `forall` there must be no more quantifiers (except, `Inferred` ones?), or * There can be extra quantifiers, but they are `Inferred`, so we'd get `f :: forall {b}. forall a. b -> a -> Bool`. (I quite like this.), or * The current behaviour. I don't feel strongly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Because GHC does not respect let-should-not-be-generalized in the
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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): '''Let-must-not-be-generalised''' behaviour presence of partial type signatures, this is rejected again. It's hard to see how GHC ''could'' respect let-should-not-be-generalised. Consider {{{ f :: forall a. _ -> a f = e }}} How could we check this signature without generalising the type of `e`? I suppose there could be a special case if there is no user-written `forall`. So `f :: forall. blah` means "please generalise` and `f :: blah` means "don't generalise". But that's in conflict with some of the choices under "forall-or-nothing" above. Regardless, it'd be good to document the behaviour in the manual. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16146: Trivial partial type signature kills type inference in the presence of GADTs -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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 goldfire): The thoughts on this ticket have led to https://github.com/ghc-proposals /ghc-proposals/pull/194 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16146#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC