[GHC] #15119: Program involving existentials and type class constraint gets rejected
#15119: Program involving existentials and type class constraint gets rejected -------------------------------------+------------------------------------- Reporter: sgraf | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.2 (Type checker) | 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: -------------------------------------+------------------------------------- The following example from https://stackoverflow.com/a/50160423/388010 demonstrates some code involving type classes and existentials that I'd love for it to pass the type checker: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} module Foo where class C a where getInt :: Int instance C Char where getInt = 42 f :: (forall a. C a => Int) -> Bool f x = even (x @ Char) g :: (forall a. C a => Int) -> Bool g = f -- fails -- g h = f h -- fails -- g h = f getInt -- fails -- g _ = f 42 -- OK }}} This complains with the following error: {{{ test.hs:17:5: error: • Could not deduce (C a0) from the context: C a bound by a type expected by the context: forall a. C a => Int at test.hs:17:5 The type variable ‘a0’ is ambiguous These potential instance exist: instance C Char -- Defined at test.hs:10:10 • In the expression: f In an equation for ‘g’: g = f | 17 | g = f -- fails | ^ }}} Is this expected behavior or a bug? I understand why the program leads to that particular error, but isn't there a way for the compiler to accept this? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15119 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15119: Program involving existentials and type class constraint gets rejected -------------------------------------+------------------------------------- Reporter: sgraf | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | 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: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): This is indeed expected. `a` is completely ambiguous in your program. The only type it ever appears in is `C a`, which is to the left of `=>`, and such types are always resolved through instance lookup, so GHC has trouble figuring out which particular instance you meant. The only type to the right of `=>`, `Int`, does not determine `a` either, so GHC throws up its hands and gives up. One way to make this program compile is to introduce an additional argument which determines `a`, such as in: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Foo where import Data.Proxy class C a where getInt :: Int instance C Char where getInt = 42 f :: (forall a. C a => Proxy a -> Int) -> Bool f x = even $ x $ Proxy @Char g :: (forall a. C a => Proxy a -> Int) -> Bool g = f }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15119#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15119: Program involving existentials and type class constraint gets rejected -------------------------------------+------------------------------------- Reporter: sgraf | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | 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: | -------------------------------------+------------------------------------- Comment (by sgraf):
`Proxy`
Well, that's what I tried to avoid in this example. There's probably no way to get what I want using only `-XTypeApplications`, right? I was the one asking the SO question which boils down to asking for a System Fw style Big lambda. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15119#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15119: Program involving existentials and type class constraint gets rejected -------------------------------------+------------------------------------- Reporter: sgraf | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | 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: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Right, you're going to need //something// which determines `a`, be it `Proxy`, `Tagged`, or something else. There may come a day in which you can write: {{{#!hs forall a -> C a => Int }}} That is, where one can make `a` a visible argument (i.e., a "big lambda", as you've put it). But until then, you'll have to resort to baser tricks to accomplish what you seek. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15119#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15119: Program involving existentials and type class constraint gets rejected -------------------------------------+------------------------------------- Reporter: sgraf | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: wontfix | 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: | -------------------------------------+------------------------------------- Changes (by sgraf): * status: new => closed * type: bug => feature request * resolution: => wontfix Comment: Let's hope that day isn't too far in the future :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15119#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC