blob: fa233247ca3cfea8cef52ce8df98cda6d6503d1e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data Foo (a :: Type) (b :: Type) where
MkFoo :: (a ~ Int, b ~ Char) => Foo a b
data family Sing (a :: k)
data SFoo (z :: Foo a b) where
SMkFoo :: SFoo MkFoo
|
