#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): `forall (f :: Type -> Type). f` is bogus. It should be rejected both by the type checker and Core Lint. This is rather awkward w.r.t. type inference (as Simon points out) because of `Constraint`. I don't like the validity-checking solution, because then we reject something like `:k forall a. a` in GHCi. `a`'s kind will be unconstrained, so it will get kind `k`. But then the `forall` is bogus. We could imagine a magic class `TypeLike` with `instance TypeLike (TYPE r)` and `instance TypeLike Constraint`. We can further imagine defaulting this class (not unlike how we default `Num`). But this is a sledgehammer of a solution, to be sure. I don't think there is anything unsound about removing the restriction... but no published type theory (to my knowledge) does so. Back in the day, the restriction wasn't there because we needed, e.g., `forall a. Array# a` -- that is, we needed unlifted types (which didn't really have kinds) in `forall`s. Now with levity polymorphism, we have a more principled way of dealing with this all, and so we do. Perhaps the new principles weren't carried all the way to their logical conclusion, though, as this ticket shows. Note: if we really can't come up with a good way to impose this restriction in the type-checker, I wouldn't be strongly opposed to just dropping it. It's just a little smelly, but no worse than that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler