blob: 6d1d0b88974f452a148b386fe06f0599fa0188cc (
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
26
27
|
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug (f) where
import Data.Kind
import Data.Proxy
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family F x :: Type -> Type
data F1Sym :: forall x a. x ~> F x a
data F2Sym :: forall x a. F x a ~> x
data Comp :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c)
sg :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Proxy f -> Proxy g -> Proxy (Comp f g)
sg _ _ = Proxy
f :: forall (x :: Type). Proxy x -> ()
f _ = ()
where
g :: forall z ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
g = sg Proxy Proxy
|
