[GHC] #15441: Data type with phantoms using TypeInType isn't coercible

26 Jul 2018


      #15441: Data type with phantoms using TypeInType isn't coercible
-------------------------------------+-------------------------------------
           Reporter:  glittershark   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.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:
-------------------------------------+-------------------------------------
 I'm *pretty* sure this is a problem with TypeInType in particular. I'd
 expect the following to compile:
 {{{#!hs
 {-# LANGUAGE GADTs, TypeInType, TypeApplications #-}
 module Bug where

 import Prelude
 import Data.Coerce
 import Data.Kind

 data Foo a = Foo

 data Bar (a :: Type) (b :: Foo a) where
   Bar :: Bar a 'Foo

 x = coerce @(Bar Int 'Foo) @(Bar Bool 'Foo)
 }}}

 But it doesn't

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