[GHC] #11282: Injectivity annotation fails in the presence of higher-rank use of constraint family

23 Dec 2015

      #11282: Injectivity annotation fails in the presence of higher-rank use of
constraint family
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.11
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 When I say

 {{{
 {-# LANGUAGE TypeFamilies, RankNTypes #-}

 module Bug where

 import GHC.Exts

 type family F a = r | r -> a
 type family G a :: Constraint

 meth :: (G a => F a) -> ()
 meth = undefined
 }}}

 I get

 {{{
 Bug.hs:10:9: error:
     • Could not deduce: F a ~ F a0
       from the context: G a0
         bound by the type signature for:
                    meth :: G a0 => F a0
         at Bug.hs:10:9-26
       NB: ‘F’ is a type function, and may not be injective
       The type variable ‘a0’ is ambiguous
     • In the ambiguity check for ‘meth’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature:
         meth :: (G a => F a) -> ()
 }}}

 The presence of `G a` is critical for exhibiting this bug. If I replace `G
 a` with `Show a` the problem disappears.

 This one was actually encountered in an attempt to do Useful Work, not
 just idle typecheckery.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11282
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler