Program involving existentials and type class constraint gets rejected
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:
{-# 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?
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |