expectJust

[goldfirere]

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, GADTs, TypeOperators,
             ScopedTypeVariables, TemplateHaskell, FlexibleInstances,
             ConstraintKinds, UndecidableInstances #-}
{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}

module Sigma where

import Data.Type.Equality
import Data.Proxy
import GHC.Exts

data family Sing (a :: k)

data Dict c where
  Dict :: c => Dict c

class SingKind k where
  type FromSing (s :: Sing (x :: k)) :: k
  type Singleton (a :: k) :: Sing a
  fromSing :: Sing (x :: k) -> k
  fromSingCorrect :: Sing x -> Sing s -> FromSing (s :: Sing (x :: k)) :~: x

class SingKind1 (t :: k -> *) where
  singKind :: forall (x :: k). Proxy (t x) -> Dict (SingKind (t x))

data Sigma (s :: *) (t :: s -> *) where
  (:&:) :: Sing (fst :: s) -> t fst -> Sigma s t

data instance Sing (x :: Sigma s t) where
  (:%&:) :: forall (s :: *) (t :: s -> *) (fst :: s) (snd :: t fst)
            (sfst :: Sing fst).
            Sing fst -> Sing snd -> Sing (sfst ':&: snd)

data instance Sing (x :: Sing b) where
  Sing :: Sing (Singleton x)

data Nat = Zero | Succ Nat

data instance Sing (n :: Nat) where
  SZero :: Sing 'Zero
  SSucc :: Sing n -> Sing ('Succ n)

data instance Sing (x :: Maybe k) where
  SNothing :: Sing 'Nothing
  SJust    :: Sing a -> Sing ('Just a)

$(return [])

instance SingKind Nat where
  type FromSing 'SZero = 'Zero
  type FromSing ('SSucc x) = 'Succ (FromSing x)

  type Singleton 'Zero = 'SZero
  type Singleton ('Succ x) = 'SSucc (Singleton x)

  fromSing SZero = Zero
  fromSing (SSucc x) = Succ (fromSing x)

  fromSingCorrect SZero Sing = Refl
  fromSingCorrect (SSucc x) Sing
    = case fromSingCorrect x Sing of Refl -> Refl

instance SingKind k => SingKind (Maybe k) where
  type FromSing 'SNothing = 'Nothing
  type FromSing ('SJust x) = 'Just (FromSing x)

  type Singleton 'Nothing = 'SNothing
  type Singleton ('Just x) = 'SJust (Singleton x)

  fromSing SNothing = Nothing
  fromSing (SJust x) = Just (fromSing x)

  fromSingCorrect SNothing Sing = Refl
  fromSingCorrect (SJust x) Sing = case fromSingCorrect x Sing of
    Refl -> Refl

instance (SingKind s, SingKind1 t) => SingKind (Sigma s t) where
  type FromSing (a ':%&: b) = a ':&: FromSing b
  type Singleton (a ':&: b) = a ':%&: Singleton b
  fromSing ((a :: Sing fst) :%&: b)
    = case singKind (Proxy :: Proxy (t fst)) of
        Dict -> a :&: fromSing b
  fromSingCorrect (a :%&: b) Sing = Refl

{-
proj1 :: Sigma s t -> s
proj1 (a :&: _) = fromSing a

type family Proj1 x where
  Proj1 (a ':&: b) = FromSing a

proj2 :: forall (s :: *) (t :: s -> *) (sig :: Sigma s t).
         Sing (sig :: Sigma s t) -> t (Proj1 sig)
proj2 (_ :%&: b) = fromSing b
-}

*** Exception: expectJust tcMatchTysX types