{-# 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 SingletonCtor (a :: k) :: Sing a
fromSing :: Sing (x :: k) -> k
fromSingCorrect :: Proxy 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).
Sing fst -> Sing snd -> Sing (fst ':&: snd)
{-
data instance Sing (x :: Sing b) where
Sing :: Sing (SingletonCtor x)
$(return [])
instance (SingKind s, SingKind1 t) => SingKind (Sigma s t) where
type FromSing (a ':%&: b) = FromSing a ':&: FromSing b
fromSing ((a :: Sing fst) :%&: b)
= case singKind (Proxy :: Proxy (t (FromSing fst))) of
Dict -> case fromSingCorrect (Proxy :: Proxy fst) of
Refl -> fromSing a :&: fromSing b
-}
{-
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
-}
yields
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 7.11.20150420 for x86_64-apple-darwin):
ASSERT failed!
file compiler/types/TyCoRep.hs line 1816
s_a8JR
[TCvSubst
In scope: InScope []
Type env: [a8JT :-> fst_a8MW]
Co env: [a8MP :-> cobox_a8MX]]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
yields