eliminators-0.6: tests/DecideTypes.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module DecideTypes where

import Data.Kind
import Data.Nat
import Data.Singletons.TH hiding (Decision(..))

-- Due to https://github.com/goldfirere/singletons/issues/82, promoting the
-- Decision data type from Data.Singletons.Decide is a tad awkward. To work
-- around these, we define a more general Decision' data type here.
data Decision' p a
  = Proved a
  | Disproved (p @@ a @@ Void)

elimDecision :: forall a (p :: PDecision a ~> Type) (d :: PDecision a).
                Sing d
             -> (forall (yes :: a). Sing yes -> p @@ Proved yes)
             -> (forall (no :: a ~> Void). Sing no -> p @@ Disproved no)
             -> p @@ d
elimDecision (SProved yes)   pProved _          = pProved yes
elimDecision (SDisproved no) _       pDisproved = pDisproved no

instance Show a => Show (Decision' p a) where
  showsPrec p (Proved a) =
    showParen (p > 10) $ showString "Proved " . showsPrec 11 a
  showsPrec p (Disproved _) =
    showParen (p > 10) $ showString "Disproved <void>"

type Decision  = Decision' (TyCon (->))
type PDecision = Decision' (~>@#@$)

data SDecision :: forall a. PDecision a -> Type where
  SProved    :: forall a (x :: a).         Sing x -> SDecision (Proved x)
  SDisproved :: forall a (r :: a ~> Void). Sing r -> SDecision (Disproved r)
type instance Sing = SDecision

instance SingKind a => SingKind (PDecision a) where
  type Demote (PDecision a) = Decision (Demote a)
  fromSing (SProved a)    = Proved (fromSing a)
  fromSing (SDisproved r) = Disproved (fromSing r)
  toSing (Proved x)    = withSomeSing x $ SomeSing . SProved
  toSing (Disproved r) = withSomeSing r $ SomeSing . SDisproved

-----

-- These newtype wrappers are needed to work around
-- https://gitlab.haskell.org/ghc/ghc/issues/9269
newtype WhyDecEqNat (k :: Nat) = WhyDecEqNat
  { runWhyDecEqNat :: forall (j :: Nat). Sing j -> Decision (k :~: j) }
newtype WhyDecEqList (l1 :: [e]) = WhyDecEqList
  { runWhyDecEqList :: forall (l2 :: [e]). Sing l2 -> Decision (l1 :~: l2) }

$(singletons [d|
  type family NatEqConsequences (a :: Nat) (b :: Nat) :: Type where
    NatEqConsequences Z      Z      = ()
    NatEqConsequences Z      (S _)  = Void
    NatEqConsequences (S _)  Z      = Void
    NatEqConsequences (S k1) (S k2) = k1 :~: k2

  type WhyNatEqConsequencesSame (a :: Nat) = NatEqConsequences a a

  type WhyDecEqZ (k :: Nat) = Decision (Z :~: k)

  type WhyDecEqS (n :: Nat) (k :: Nat) = Decision (S n :~: k)

  type family ListEqConsequences (xxs :: [e]) (yys :: [e]) :: Type where
    ListEqConsequences '[]    '[]    = ()
    ListEqConsequences '[]    (_:_)  = Void
    ListEqConsequences (_:_)  '[]    = Void
    ListEqConsequences (x:xs) (y:ys) = (x :~: y, xs :~: ys)

  type WhyListEqConsequencesSame (es :: [e]) = ListEqConsequences es es

  type WhyDecEqNil (es :: [e]) = Decision ('[] :~: es)

  type WhyDecEqCons (x :: e) (xs :: [e]) (es :: [e]) = Decision ((x:xs) :~: es)

  type WhyIntermixListEqs1 (x :: e) (xs :: [e]) (ys :: [e]) (k :: e) = (x:xs) :~: (k:ys)
  type WhyIntermixListEqs2 (x :: e) (xs :: [e]) (k :: [e])           = (x:xs) :~: (x:k)
  |])