ghci SOP.hs

SOP.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import           GHC.Types
import           GHC.TypeLits

data NS (a :: k -> Type) (b :: [k]) where
  Z :: forall k (a :: k -> Type) (x :: k) (xs :: [k]). (a x) -> NS a (x : xs)
data NP (a :: k -> Type) (b :: [k]) where
  S :: forall k (a :: k -> Type) (x :: k) (xs :: [k]). (a x) -> NP a (x : xs)

type family IndexNP np ns where
  -- IndexNP (NP f (x:_))  (NS _ (y:'[])) = TypeError (Text "Boo.")
  IndexNP  np            ns            = TypeError (Text "Irreducible.")

--  As expected:
*Main> :kind! forall f x1 xs1 g x2 xs2. IndexNP (NP f (x1 : xs1)) (NS g (x2 : xs2))
forall f x1 xs1 g x2 xs2. IndexNP (NP f (x1 : xs1)) (NS g (x2 : xs2)) :: k
= (TypeError ...)

---
--- Now, let's add a clause to the family:
---

type family IndexNP np ns where
  IndexNP (NP f (x:_))  (NS _ (y:'[])) = TypeError (Text "Boo.")
  IndexNP  np            ns            = TypeError (Text "Irreducible.")

--  Not expected:
*Main> :kind! forall f x1 xs1 g x2 xs2. IndexNP (NP f (x1 : xs1)) (NS g (x2 : xs2))
forall f x1 xs1 g x2 xs2. IndexNP (NP f (x1 : xs1)) (NS g (x2 : xs2)) :: k
= IndexNP (NP f (x1 : xs1)) (NS g (x2 : xs2))