Skip to content

Data type with phantoms using TypeInType isn't coercible

I'm *pretty* sure this is a problem with TypeInType in particular. I'd expect the following to compile:

{-# 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

Trac metadata
Trac field Value
Version 8.4.2
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information