[GHC] #14921: Type inference breaks on constraint-kinded parameter used by a Rank-2 callback
#14921: Type inference breaks on constraint-kinded parameter used by a Rank-2 callback -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Apologies in advance if the terminology in the summary is incorrect, I'm not really sure of the proper terms to use here The following code: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ScopedTypeVariables #-} module Scratch where import Prelude data Foo = FooA Int | FooB String useFoo :: forall cls a . (cls Int, cls String) => (forall k . cls k => k -> a) -> Foo -> a useFoo f (FooA a) = f a useFoo f (FooB b) = f b }}} seems like it should be able to infer the `cls` type parameter to `useFoo` based on the first argument, but instead calling with `kshow` gives the following error message: {{{#!hs
useFoo show (FooA 1)
<interactive>:52:1: error: • Could not deduce: (cls0 Int, cls0 String) arising from a use of ‘useFoo’ • In the expression: useFoo show (FooA 1) In an equation for ‘it’: it = useFoo show (FooA 1) <interactive>:52:8: error: • Couldn't match type ‘a’ with ‘String’ ‘a’ is untouchable inside the constraints: cls0 k bound by a type expected by the context: forall k. cls0 k => k -> a at <interactive>:52:1-20 ‘a’ is a rigid type variable bound by the inferred type of it :: a at <interactive>:52:1-20 Possible fix: add a type signature for ‘it’ Expected type: k -> a Actual type: k -> String • In the first argument of ‘useFoo’, namely ‘show’ In the expression: useFoo show (FooA 1) In an equation for ‘it’: it = useFoo show (FooA 1) • Relevant bindings include it :: a (bound at <interactive>:52:1) }}} Type-applying `useFoo` works as expected: {{{#!hs
:set -XTypeApplications useFoo @Show show (FooA 1) "1" }}}
This broke both with and without ScopedTypeVariables -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14921 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14921: Type inference breaks on constraint-kinded parameter used by a Rank-2 callback -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #10651 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #10651 Comment: This is more or less expected behavior. See #10651 for a similar scenario. In general, GHC doesn't unify underneath equalities or something that might turn into an equality, such as `cls k` (this is why `a` is untouchable in your error message, as you'd have to unify it underneath `cls k`). As SPJ notes in https://ghc.haskell.org/trac/ghc/ticket/10651#comment:2, this limitation is explained in Section 5 of the [http://research.microsoft.com/~simonpj/papers/constraints/jfp- outsidein.pdf OutsideIn paper], and it's unknown how to improve this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14921#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14921: Type inference breaks on constraint-kinded parameter used by a Rank-2 callback -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #10651, #15649 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid * related: #10651 => #10651, #15649 Comment: I'm going to close this, since the fact that this program doesn't typecheck is expected behavior (at least, according to the specification in the OutsideIn(X) paper, as explained in https://ghc.haskell.org/trac/ghc/ticket/10651#comment:2). See also #10651 and #15649, which are similar tickets. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14921#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14921: Type inference breaks on constraint-kinded parameter used by a Rank-2 callback -------------------------------------+------------------------------------- Reporter: glittershark | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #10651, #15649 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by infinity0): As mentioned on the other tickets `Proxy` is an alternative workaround to `TypeApplications` + `AllowAmbiguousTypes`, the latter being quite a strong relaxation that one often doesn't want to enable in library code. {{{#!haskell {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ScopedTypeVariables #-} module Scratch where import Data.Proxy import Prelude data Foo = FooA Int | FooB String useFoo :: forall cls a . (cls Int, cls String) => Proxy cls -> (forall k . cls k => k -> a) -> Foo -> a useFoo _ f (FooA a) = f a useFoo _ f (FooB b) = f b x = useFoo (Proxy :: Proxy Show) show (FooA 1) }}} compiles without errors. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14921#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC