GADTs example

anonymous-gist.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

module GADTs where

data Subject = Math | English | French
  deriving (Eq, Show)

class MathOrEnglish (a :: Subject)
instance MathOrEnglish 'Math
instance MathOrEnglish 'English

data User a where
  Teacher :: Subject -> User a
  
  -- Uncommenting line 25 below gives the error:
  -- • Expected a type, but ‘a’ has kind ‘Subject’
  -- • In the type ‘a’
  -- In the definition of data constructor ‘Student’
  -- In the data declaration for ‘User’ (lsp)
  
  -- Student :: (MathOrEnglish a) => a -> User a -- doesn't work

  Student :: (Eq a) => a -> User a -- works