#15710: Should GHC accept a type signature that needs coercion quantification? -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType 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 changed by simonpj: Old description:
Consider {{{ f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x f = error "uk" }}} Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being {{{ f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1->*)). (f |> co) x }}} But there is a problem: the user wrote `k ~ (k1 -> *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here.
New description: Consider {{{ f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x f = error "uk" }}} Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being {{{ f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1->*)). (f |> co) x }}} But there is a problem: the user wrote `k ~ (k1 -> *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here. These thoughts arose when contemplating `Note [Emitting the residual implication in simplifyInfer]` in `TcSimplify`; see comment:5 in #15497 -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15710#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler