blob: c05bd3a8a023081efa5c883a026b0b2979f79966 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module T15122 where
import Data.Kind
import Data.Proxy
data IsStar (a :: k) where
IsStar :: IsStar (a :: Type)
type family F (a :: k) :: k
foo :: (F a ~ F b) => IsStar a -> Proxy b
-> Proxy (F a) -> Proxy (F b)
foo IsStar _ p = p
|
