blob: 18ebc42f92d7b027342205dc669269b9639e0bcd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Proxy
import Data.Type.Equality
type family F (x :: f (a :: k)) :: f a
f :: forall k (f :: k -> Type) (a :: k) (r :: f a). Proxy r -> F r :~: r
f = undefined
g :: forall (f :: Type -> Type) (a :: Type) (r :: f a). Proxy r -> F r :~: r
g r | Refl <- f -- Uncommenting the line below makes it work again
-- @Type
@f @a @r r
= Refl
|
