[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 RyanGlScott):

 The culprit appears to be
 [http://git.haskell.org/ghc.git/blob/ebb7613a66a784fc0015e13a6379453e6d5af44d:/compiler/typecheck/TcValidity.hs#l536
 these lines] of `check_syn_tc_app`:

 {{{#!hs
   = do  { -- See Note [Liberal type synonyms]
         ; liberal <- xoptM LangExt.LiberalTypeSynonyms
         ; if not liberal || isTypeFamilyTyCon tc then
                 -- For H98 and synonym families, do check the type args
                 mapM_ check_arg tys

           else  -- In the liberal case (only for closed syns), expand then
 check
           case tcView ty of
              Just ty' -> let syn_tc = fst $ tcRepSplitTyConApp ty
                              err_ctxt = text "In the expansion of type
 synonym"
                                         <+> quotes (ppr syn_tc)
                          in addErrCtxt err_ctxt $ check_type env ctxt rank
 ty'
              Nothing  -> pprPanic "check_tau_type" (ppr ty)  }
 }}}

 When checking a type synonym application (like `Foo`) without
 `LiberalTypeSynonyms` enabled, then we don't check the expanded type at
 all—we only check the arguments! As a consequence, we never validity-check
 the underlying `Eq b => b` that is lurking behind the scenes in `f ::
 forall b (a :: Foo b). Int`. (This also reveals that enabling
 `LiberalTypeSynonyms` will cause the program to be rejected as well.)

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