#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