blob: 0f4161db7231b6f2620b929d56a799e0c5f38768 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
module T22235 (f) where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..))
f :: ST x -> ST y -> x :~: y
f st1@SMkT st2@SMkT = method st1 st2
type T :: Type -> Type
data T a where
MkT :: T Int
type ST :: T a -> Type
data ST (t :: T a) where
SMkT :: ST MkT
class C f where
method :: f a -> f b -> a :~: b
instance C ST where
method SMkT SMkT = Refl
|
