#13337: GHC doesn't think a type is of kind *, despite having evidence for it -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Forgive me if this is a silly question, but why shouldn't the first example work? I know that the implementation details would significantly complicate the story, but my perspective, being able to write the first example would make a lot of code easier to write. An example of this that came up in real code is when [https://mail.haskell.org/pipermail/ghc- devs/2017-February/013850.html Edward Kmett tried to sketch out a solution] to #13327 on the ghc-devs mailing list, and attempted to write this code: {{{#!hs class (Typeable t, Typeable k) => DataIfStar (k :: t) where dataIf :: (t ~ Type) => proxy k -> (Data k => r) -> r }}} But this won't work, because `Data :: Type -> Constraint`, and GHC isn't able to conclude that `k :: t` is actually `k :: Type`, since the evidence that `t ~ Type` isn't being used when typechecking. If programs like these aren't supposed to typecheck by design, what is the workaround? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13337#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler