Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T8566a.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE PolyKinds #-}
3 {-# LANGUAGE TypeFamilies #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeOperators #-}
7 module T8566a where
8
9 import Data.Kind (Type)
10
11 data Field = forall k. APP k [Field]
12
13 data InField (u :: Field) :: Type where
14 A :: AppVars t (ExpandField args) -> InField (APP t args)
15
16 type family ExpandField (args :: [Field]) :: [Type]
17 type family AppVars (t :: k) (vs :: [Type]) :: Type
18
19 -- This function fails to compile, because we discard
20 -- 'given' kind equalities. See comment 7 in Trac #8566
21 -- This is really a bug, I claim
22 unA :: InField (APP t args) -> AppVars t (ExpandField args)
23 unA (A x) = x
24