[GHC] #15979: Core Lint error with LiberalTypeSynonyms

[GHC]

#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