Opened 14 months ago

Last modified 14 months ago

#15441 new feature request

Data type with phantoms using TypeInType isn't coercible

Reported by: glittershark Owned by:
Priority: normal Milestone: Research needed
Component: Compiler Version: 8.4.2
Keywords: Roles Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (6)

comment:1 Changed 14 months ago by goldfire

You're implicitly suggesting that the first parameter to Bar can be assigned a phantom role. Currently, all dependent parameters are assigned a nominal role. Perhaps you're right that a phantom role there would be sound, but we have not worked out the theory fully for this case. Inferring nominal there is safe, so that's what we do today. Perhaps tomorrow, we'll do better, but we'll need a big proof before we can do it with confidence.

comment:2 Changed 14 months ago by glittershark

As a follow-up with further information, the code where I'm actually using this has Foo as a GADT, where the constructor I'm coercing has its parameter phantom, like so:

{-# LANGUAGE GADTs, TypeInType, TypeApplications #-}
module Coerce where

import Prelude
import Data.Coerce
import Data.Kind

data Foo (a :: Type) where
  A :: Foo a
  C :: Foo Int

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

x = coerce @(Bar Int 'A) @(Bar Bool 'A)

comment:3 Changed 14 months ago by glittershark

Yeah, after discussing this a little in #haskell this looks more like a feature request than a bug report

comment:4 Changed 14 months ago by goldfire

Keywords: Roles added

That looks even more suspect -- my guess is that inferring a phantom there wouldn't be sound.

Hopefully we'll have a worked out theory for roles and dependency in the next few months (there's active work going on here), but we're not there yet.

comment:5 Changed 14 months ago by monoidal

Type: bugfeature request

comment:6 Changed 14 months ago by RyanGlScott

Milestone: 8.6.1Research needed
Note: See TracTickets for help on using tickets.