blob: a452bef0df8809989d43ac1a2d5581392b4095ff (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module T15453 where
import Data.Kind
import Data.Proxy
import Data.Type.Equality
type family S :: Type where
S = T
type family T :: Type where
T = Int
f :: (forall (x :: S). Proxy x) :~: (forall (x :: T). Proxy x)
f = Refl
g :: (forall (x :: T). Proxy x) :~: (forall (x :: Int). Proxy x)
g = Refl
h :: (forall (x :: S). Proxy x) :~: (forall (x :: Int). Proxy x)
h = f `trans` g
|