#7503: Bug with PolyKinds, type synonyms & GADTs -------------------------------------+------------------------------------- Reporter: Ashley Yakeley | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.6.1 checker) | Keywords: GADTs, Resolution: | TypeInType Operating System: Linux | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: #14451 | Differential Rev(s): Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference| -------------------------------------+------------------------------------- Comment (by RyanGlScott): Continuing my journey started in https://ghc.haskell.org/trac/ghc/ticket/14451#comment:7, it appears that something changed between GHC 8.4 and 8.6 that affects the programs in this ticket. Amazingly, the original program: {{{#!hs {-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #-} module TestConstraintKinds where import GHC.Exts hiding (Any) data WrappedType = forall a. WrapType a data A :: WrappedType -> * where MkA :: forall (a :: *). AW a -> A (WrapType a) type AW (a :: k) = A (WrapType a) type AW' (a :: k) = A (WrapType a) class C (a :: k) where aw :: AW a -- workaround: AW' instance C [] where aw = aw }}} Now typechecks with GHC 8.6.2 and HEAD! Unfortunately, it might be too early to declare victory here, since the program in comment:1: {{{#!hs {-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #-} module TestConstraintKinds where data Wrap a -- Wrap :: forall k. k -> * data A a = MkA a (AW a) type AW a = A (Wrap a) type AW2 a = A (Wrap a) class C (a :: k) where aw :: AW a }}} Still refuses to typecheck, even on GHC 8.6.2 and HEAD. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/7503#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler