[GHC] #15119: Program involving existentials and type class constraint gets rejected

4 May 2018

      #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