content: {-# LANGUAGE DataKinds      #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE TypeFamilies   #-}
  
  {-# OPTIONS_GHC -fplugin=Type.Compare.Plugin #-}
  
  module ShouldTypecheck where
  
  import           Data.Proxy
  import           GHC.TypeLits
  import qualified Prelude as P
  import           Prelude hiding (Int)
  import           Type.Compare
  
  
  testSym1 :: Proxy (CmpType "a" "apple") -> Proxy 'LT
  testSym1 = id
  
  testSym2 :: Proxy (CmpType "banana" "banana") -> Proxy 'EQ
  testSym2 = id
  
  testSym3 :: Proxy (CmpType "dominos" "cabana") -> Proxy 'GT
  testSym3 = id
  
  
  testNat1 :: Proxy (CmpType 0 1) -> Proxy 'LT
  testNat1 = id
  
  testNat2 :: Proxy (CmpType 2 2) -> Proxy 'EQ
  testNat2 = id
  
  testNat3 :: Proxy (CmpType 4 3) -> Proxy 'GT
  testNat3 = id
  
  
  data Apricot
  data Blueberry
  data Coconut
  data Durian
  
  testType1 :: Proxy (CmpType Apricot Blueberry) -> Proxy 'LT
  testType1 = id
  
  testType2 :: Proxy (CmpType Coconut Coconut) -> Proxy 'EQ
  testType2 = id
  
  testType3 :: Proxy (CmpType Durian Coconut) -> Proxy 'GT
  testType3 = id
  
  
  type family IsEQ (ord :: Ordering) :: Bool where
    IsEQ 'EQ = 'True
    IsEQ _   = 'False
  
  testType4 :: Proxy (IsEQ (CmpType Durian Coconut)) -> Proxy 'False
  testType4 = id
  
  testType5 :: Proxy (IsEQ (CmpType Blueberry Blueberry)) -> Proxy 'True
  testType5 = id
  
  testType6 :: Proxy (CmpType [Apricot] [Blueberry]) -> Proxy 'LT
  testType6 = id
  
  testType7 :: Proxy (CmpType [Durian] [Coconut]) -> Proxy 'GT
  testType7 = id
  
  testType8 :: Proxy '[CmpType [Durian] [Coconut]] -> Proxy '[ 'GT ]
  testType8 = id
  
  testType9 :: Proxy '[IsEQ (CmpType [Durian] [Coconut])] -> Proxy '[ 'False ]
  testType9 = id
  
  testType10 :: Proxy '[IsEQ (CmpType [[Apricot]] [[Apricot]])] -> Proxy '[ 'True ]
  testType10 = id
  
  testType11 :: Proxy '[IsEQ (CmpType [Apricot] [[Apricot]])] -> Proxy '[ 'False ]
  testType11 = id
  
  
  data Int
  
  testType12 :: Proxy (IsEQ (CmpType Int P.Int)) -> Proxy 'False
  testType12 = id
  
  testType13 :: Proxy (IsEQ (CmpType '[Int] '[P.Int])) -> Proxy 'False
  testType13 = id
  
  testType14 :: Proxy (CmpType '(Int, Int) '(Int, Bool)) -> Proxy 'GT
  testType14 = id
  
  testType15 :: Proxy (CmpType '[Int, Bool] '[Int, Bool]) -> Proxy 'EQ
  testType15 = id
  
  testType16 :: Proxy (CmpType '[Int, Int] '[Int, Bool]) -> Proxy 'GT
  testType16 = id
  
  -- NOTE(sandy): I don't really understand why this one is so...
  testType17 :: Proxy (CmpType '[Int, Bool] '[]) -> Proxy 'LT
  testType17 = id
  
  testType18 :: Proxy (CmpType '(String, Bool, '(Int, Bool, String), Int)
                               '(String, Bool, '(Int, Char, String), Int)) -> Proxy 'LT
  testType18 = id
  
  testType19 :: Proxy (CmpType '(String, Bool, '(Int, Char, String), Int)
                               '(String, Bool, '(Int, Bool, String), Int)) -> Proxy 'GT
  testType19 = id
  
  testType20 :: Proxy (CmpType '(String, Bool, '(Int, Char, String), Int)
                               '(String, Bool, '(Int, Char, String), Int)) -> Proxy 'EQ
  testType20 = id
  
  testType21 :: Proxy (CmpType '(String, Bool, '(Int, "a", String), Int)
                               '(String, Bool, '(Int, "b", String), Int)) -> Proxy 'LT
  testType21 = id
  
  testType22 :: Proxy (CmpType '(String, Bool, '(Int, "b", String), Int)
                               '(String, Bool, '(Int, "b", String), Int)) -> Proxy 'EQ
  testType22 = id
  
  testType23 :: Proxy (CmpType (Proxy "banana") (Proxy Int)) -> Proxy 'GT
  testType23 = id
  