Re: [GHC] #12466: Typechecker regression: Inaccessible code in a type expected by the context

8 Aug 2016

      #12466: Typechecker regression: Inaccessible code in a type expected by the context
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.1
  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):

 Huh, I didn't think that manually implementing `foo` would fix the issue,
 but sure enough, this compiles without warnings on GHC HEAD:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 module Bug where

 class Foo a where
   foo :: (a ~ Int => Int) -> a -> a
   foo _ a2 = a2

 instance Foo Char where
   foo _ a2 = a2
 }}}

 What I don't understand is how this code is any different from the default
 implementation. If the default implementation succeeds or fails, shouldn't
 copy-and-pasting it behave likewise?

 Even stranger, adding the type signature manually via `InstanceSigs`
 causes it to fail to typecheck again:

 {{{#!hs
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 module Bug where

 class Foo a where
   foo :: (a ~ Int => Int) -> a -> a
   foo _ a2 = a2

 instance Foo Char where
   foo :: (Char ~ Int => Int) -> Char -> Char
   foo _ a2 = a2
 }}}

 {{{
 $ /opt/ghc/head/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:11:10: error:
     • Couldn't match type ‘Char’ with ‘Int’
       Inaccessible code in
         the type signature for:
           foo :: Char ~ Int => Int
     • In the ambiguity check for ‘foo’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature: foo :: (Char ~ Int => Int) -> Char -> Char
       In the instance declaration for ‘Foo Char’

 Bug.hs:11:10: error:
     • Couldn't match type ‘Char’ with ‘Int’
       Inaccessible code in
         the type signature for:
           foo :: Char ~ Int => Int
     • When checking that instance signature for ‘foo’
         is more general than its signature in the class
         Instance sig: (Char ~ Int => Int) -> Char -> Char
            Class sig: (Char ~ Int => Int) -> Char -> Char
       In the instance declaration for ‘Foo Char’
 }}}

 So I'm quite lost as to what's happening, and moreover, what //should//
 happen.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12466#comment:9
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler