[GHC] #16059: checkValidType is defeated by a type synonym

[GHC]

#16059: checkValidType is defeated by a type synonym
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.7
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC accepts       |  Unknown/Multiple
  invalid program                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 The problem in this code

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 module Bug where

 type Foo b = Eq b => b

 f :: forall b (a :: Foo b). Int
 f = 42
 }}}

 is the ''definition'' of `Foo`, not the usage of it. As comment:3
 illustrates and comment:4 elaborates, we don't really want to check the
 expansion of a type synonym in this way. (Hold off on considering
 `LiberalTypeSynonyms` for now.) Even with the rather transparent
 interpretation of type synonyms in GHC, I think they should offer ''some''
 level of abstraction (in contrast to the position in comment:4): it seems
 that allowing type synonyms at least to hide what extensions are enabled
 is sensible.

 What about `LiberalTypeSynonyms`? I don't know. But let's see if we can
 agree on conservative synonyms first, and then we'll move to liberal ones.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16059#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler