Re: [GHC] #14333: GHC doesn't use the fact that Coercible is symmetric

8 Oct 2017

      #14333: GHC doesn't use the fact that Coercible is symmetric
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * cc: RyanGlScott (added)
 * keywords:   => TypeFamilies

Comment:

 Indeed, something funny is going on here.

 Here's a simplified version of this program. Notice that this typechecks:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}

 import Data.Type.Coercion

 type family F a b :: *

 f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b)
 f Coercion = Coercion
 }}}

 However, if you change the kind of `F`:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}

 import Data.Type.Coercion

 type family F a :: * -> *

 f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b)
 f Coercion = Coercion
 }}}

 Then it no longer typechecks:

 {{{
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/ryanglscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 Bug.hs:10:14: error:
     • Could not deduce: Coercible (F c d) (F a b)
         arising from a use of ‘Coercion’
       from the context: Coercible (F a b) (F c d)
         bound by a pattern with constructor:
                    Coercion :: forall k (a :: k) (b :: k).
                                Coercible a b =>
                                Coercion a b,
                  in an equation for ‘f’
         at Bug.hs:10:3-10
       NB: ‘F’ is a type function, and may not be injective
     • In the expression: Coercion
       In an equation for ‘f’: f Coercion = Coercion
     • Relevant bindings include
         f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b)
           (bound at Bug.hs:10:1)
    |
 10 | f Coercion = Coercion
    |              ^^^^^^^^
 }}}

 Of course, it's quite easy to actually construct an implementation of `f`
 which does typecheck:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}

 import Data.Type.Coercion

 type family F a :: * -> *

 f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b)
 f = sym
 }}}

 So the mystery is why GHC gets tripped up on this particular incarnation
 of `F`.

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