Haskell equivalent of Kotlin's invariant types

Question

In Kotlin i can do

sealed class Substance {
    object Uranus : Substance()
    object Mercury: Substance()
    object Ammonia : Substance()
}

data class DangerousBox<T : Substance>(val item: T)

fun main() {
    val uranus = DangerousBox<Substance.Uranus>(Substance.Uranus)
    val mercury: DangerousBox<Substance.Mercury> = uranus
}

Now i have invariant types DangerousBox<Substance.Uranus>, DangerousBox<Substance.Mercury> etc., so sample above would't compile.

How make it in Haskell?

Ideally i would like to have types

uranus :: DangerousBox Uranus
uranus = DangerousBox Mercury

and this sample musn't comlie too.

I tried to achieve it in the following ways:

1. Modular constraint. I have module

module Sample.Types.Boxes
  ( Substance(..)
  , dangerousBox
  , VDangerousBox {- no Con-}
  ) where

data Substance
  = Uranus
  | Mercury
  | Ammonia
  deriving (Show)

data VDangerousBox a =
  VDangerousBox Substance
  deriving (Show)

dangerousBox :: Substance -> VDangerousBox Substance
dangerousBox a = VDangerousBox a

Clients of module can use only dangerousBox, but here i have jeneric in relation to Substance:

uranus :: VDangerousBox Substance
uranus = dangerousBox Uranus

2. Data kinds

data DangerousBox :: Substance -> * where
  DangerousBox :: Substance -> DangerousBox a

uranus :: DangerousBox Uranus
uranus = DangerousBox Uranus

mercury :: DangerousBox Mercury
mercury = uranus {- it's ok, it dosn't compile -}

But in this case the following case will compile:

mercury :: DangerousBox Mercury
mercury = DangerousBox Ammonia

I understand that i received equivalent for

data Box<T : Substance>(val value: Substance)

in term of Kotlin generics it.

It's no real case, it is only of "academic" interest.

Answer 1

Since, given a particular choice of substance, there isn't any other information to be contained in the box (at least in your Kotlin code), I'd first consider just omitting it entirely:

import Data.Kind (Type)  -- preferred version instead of the old *

data DangerousBox :: Substance -> Type where
  DangerousBox :: DangerousBox a

uranus :: DangerousBox Uranus
uranus = DangerousBox

Then the mercury = DangerousBox Ammonia problem can't even arise, because the DangerousBox value constructor doesn't take any arguments.

If for some reason you do need an actual value representing the tag-type, then this should not be the tag itself as a Type-value, because in that view Uranus, Mercury and Ammonia are all the same type. Instead, you should use what's normally called the singletons of these types. You could have them auto-generated, or define them manually:

data SubstanceSing :: Substance -> Type where
  UranusS :: SubstanceSing 'Uranus
  MercuryS :: SubstanceSing 'Mercury
  AmmoniaS :: SubstanceSing 'Ammonia

Now UranusS corresponds to your Kotlin Substance.Uranus when appearing on the value-level. Your box type then becomes

data DangerousBox :: Substance -> Type where
  DangerousBox :: SubstanceSing a -> DangerousBox a