summaryrefslogtreecommitdiff
path: root/testsuite/tests/dependent/should_compile/T12176.hs
blob: 8c73918905d3039ccbbfc225557776ed2db43f34 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies,
             StandaloneKindSignatures #-}

module T12176 where

import Data.Kind

data Proxy :: forall k. k -> Type where
  MkProxy :: forall k (a :: k). Proxy a

data X where
  MkX :: forall (k :: Type) (a :: k). Proxy a -> X

type Expr :: forall (a :: Bool). Proxy a -> X
type Expr = MkX :: forall (a :: Bool). Proxy a -> X

type family Foo (x :: forall (a :: k). Proxy a -> X) where
  Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)

type Bug = Foo Expr  -- this failed with #12176