[GHC] #13083: Constraint solving failure with Coercible + type family + newtype

7 Jan 2017


      #13083: Constraint solving failure with Coercible + type family + newtype
-------------------------------------+-------------------------------------
           Reporter:  conal          |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:  Coercible      |  Operating System:  MacOS X
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I'm getting a type error using `coerce` to remove the wrapper of a
 `newtype` specialization involving a the following. See below for the
 smallest example I was able to construct.
 {{{#!hs
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}

 {-# OPTIONS_GHC -Wall #-}

 -- | Bug(?) in Coercible constraint solving

 -- module B2 where

 import GHC.Generics (Par1(..),(:*:)(..))
 import GHC.Exts (coerce)

 -- Representation as free vector space
 type family V (a :: *) :: * -> *

 type instance V Float = Par1
 type instance V (a,b) = V a :*: V b

 type instance V (Par1 a) = V a
 type instance V ((f :*: g) a) = V (f a, g a)

 --     • Variable ‘a’ occurs more often
 --         in the type family application ‘V (f a, g a)’
 --         than in the instance head
 --       (Use UndecidableInstances to permit this)

 type R = Float

 -- Linear map in row-major order
 newtype L a b = L (V b (V a R))

 -- Use coerce to drop newtype wrapper
 bar :: L a b -> V b (V a R)
 bar = coerce

 {--------------------------------------------------------------------
     Bug demo
 --------------------------------------------------------------------}

 -- A rejected type specialization of bar with a ~ (R,R), b ~ (Par1 R,R)
 foo :: L (R,R) (Par1 R,R) -> V (Par1 R,R) (V (R,R) R)
 foo = coerce

 --     • Couldn't match representation of type ‘V Par1’
 --                                with that of ‘Par1’
 --         arising from a use of ‘coerce’

 -- Note that Par1 has the wrong kind (* -> *) for V Par1

 -- Same error:
 --
 -- foo :: (a ~ (R,R), b ~ (Par1 R,R)) => L a b -> V b (V a R)

 -- The following similar signatures work:

 -- foo :: L (R,R) (R,Par1 R) -> V (R,Par1 R) (V (R,R) R)
 -- foo :: L (Par1 R,R) (R,R) -> V (R,R) (V (Par1 R,R) R)

 -- Same error:

 -- -- Linear map in column-major order
 -- newtype L a b = L (V a (V b s))

 -- foo :: L (R,R) (Par1 R,R) -> V (R,R) (V (Par1 R,R) R)
 -- foo = coerce
 }}}

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