HasNat.hs

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators        #-}

{-# OPTIONS_GHC -Wall -Wno-missing-methods #-}

module HasNat where

import           GHC.TypeLits        (Nat)
import           GHC.Types           (type (~~))
import           Type.Errors         (ErrorMessage(Text), TypeError)

-- Types from which we'd like to extract the "Nat"
data ContainsNat1 (a :: Nat) = ContainsNat1 deriving Show
data ContainsNat2 (a :: Nat) = ContainsNat2 deriving Show

-- Class with associated type that's able to extract nats from types
class HasNat r where
  type GetNat r :: Nat

-- Custom type error if no instance was found
type NoHasNatFound = 'Text "You dun goofed"
instance {-# OVERLAPPABLE #-} TypeError NoHasNatFound => HasNat a

-- Instances for atomic types we know to have nats
instance HasNat (ContainsNat1 a) where
  type GetNat (ContainsNat1 a) = a

instance HasNat (ContainsNat2 a) where
  type GetNat (ContainsNat2 a) = a

-- Tuple instance ONLY when nats are equal across the board
instance (GetNat a ~~ GetNat b) => HasNat (a, b) where
  type GetNat (a, b) = GetNat a

getNat :: HasNat r => r -> r
getNat r = r

-- GOAL:
--
-- >>>  :set -XTypeApplications -XDataKinds
-- >>> getNat (ContainsNat1 @3, ContainsNat2 @5)
-- <interactive>:2:1: error:
--    • You dun goofed
--    • In the expression: getNat (ContainsNat1 @3, ContainsNat2 @5)
--      In an equation for ‘it’: it = getNat (ContainsNat1 @3, ContainsNat2 @5)