[GHC] #14921: Type inference breaks on constraint-kinded parameter used by a Rank-2 callback

14 Mar 2018


      #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