Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T8566.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE PolyKinds #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE FlexibleInstances #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeOperators #-}
7 {-# LANGUAGE UndecidableInstances #-}
8 {-# LANGUAGE MultiParamTypeClasses #-}
9 {-# LANGUAGE AllowAmbiguousTypes #-} -- 'c' is ambiguous
10
11 module T8566 where
12
13 import Data.Kind (Type)
14
15 data U (s :: Type) = forall v. AA v [U s]
16 -- AA :: forall (s:*) (v:*). v -> [U s] -> U s
17
18 data I (u :: U Type) (r :: [Type]) :: Type where
19 A :: I (AA t as) r -- Existential k
20
21 -- A :: forall (u:U *) (r:[*]) Universal
22 -- (k:BOX) (t:k) (as:[U *]). Existential
23 -- (u ~ AA * k t as) =>
24 -- I u r
25
26 -- fs unused, but needs to be present for the bug
27 class C (u :: U Type) (r :: [Type]) (fs :: [Type]) where
28 c :: I u r -> I u r
29
30 -- c :: forall (u :: U *) (r :: [*]) (fs :: [*]). C u r fs => I u r -> I u r
31
32 instance (C (AA (t (I a ps)) as) ps fs) => C (AA t (a ': as)) ps fs where
33 -- instance C (AA t (a ': as)) ps fs where
34 c A = c undefined