{-# LANGUAGE AllowAmbiguousTypes, DataKinds, PolyKinds, ScopedTypeVariables, TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators #-}
-- {-# OPTIONS_GHC -ddump-splices #-}

module Main where

import Data.Type.Bool
import GHC.TypeNats

import Fcf.Core
import Fcf.Family
import Fcf.Family.TH

fcfify ''(||)
fcfify ''(+)
fcfify ''If

type family Fst (xs :: (k, l)) :: k where Fst '(x, _) = x
type family Snd (xs :: (k, l)) :: l where Snd '(_, y) = y

fcfify ''Fst
fcfify ''Snd

type (:+:) = MkName "base" "GHC.TypeNats" "+"
type If_ = MkName "base" "Data.Type.Bool" "If"

equals :: forall a b. (a ~ b) => IO ()
equals = pure ()

main :: IO ()
main = do
  equate @(Eval (Family (:+:) P0 '(1, '(2, '())))) @3
  equate @(Eval (Family If_ P1 '( 'True , '(1, '(2, '()))))) @1
  equate @(Eval (Family If_ P1 '( 'False, '(1, '(2, '()))))) @2

  -- Test applyFamily
  equals @(Eval $(applyFamily ''(+) [ [t|3|] , [t|4|] ])) @7
  equals @(Eval $(applyFamily ''If [ [t|'True|] , [t|Int|] , [t|()|] ])) @Int

  -- Test kind inference: the two Any under If should have the same type.
  equate @(Eval (Family If_ P1 '( 'True, '(Any, '(Any, '()))))) @Any

  -- The following should fail because Family_ is untyped (unlike Family)
  -- equate @(Eval (Family_ If_ P1 '( 'True, '(Any, '(Any, '()))))) @Any

-- Utils

type family Any :: k where {}

equate :: forall a b. (a ~ b) => IO ()
equate = pure ()