blob: ed87035b244eb2fa9190a59aafedea506ee71850 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
{-# Language TypeInType, TypeFamilies, TypeOperators #-}
module T14520 where
import Data.Kind
type a ~>> b = (a, b) -> Type
data family Sing (a::k)
type family XXX (f::a~>>b) (x::a) :: b
type family Id :: (kat :: a ~>> (a ~>> *)) `XXX` (b :: a) `XXX` b
sId :: Sing w -> Sing (Id :: bat w w)
sId = sId
|
