Pokemon.hs

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
module Pokemon where

import Data.Kind (Type)
import Data.Void (Void)
import Type.Reflection ((:~:)(..))

data PokemonType = None | Fire | Water | Grass

data Pokemon (a :: PokemonType) (b :: PokemonType) where
  Poke :: (a :~: b -> Void) -> Pokemon a b

bulbasaur :: Pokemon Grass None
bulbasaur= Poke (\case {})

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
module Demo where

import Data.Kind (Type, Constraint)
import Data.Void (Void)
import Type.Reflection ((:~:)(..))

data PokemonType = None | Fire | Water | Grass

type family Different a b :: Constraint where
  Different a a = () ~ Int
  Different a b = ()

data Pokemon (a :: PokemonType) (b :: PokemonType) where
  Poke :: Different a b => Pokemon a b

charmander :: Pokemon Fire None
charmander = Poke