Re: [GHC] #15954: LiberalTypeSynonyms unsaturation check doesn't kick in

26 Nov 2018

      #15954: LiberalTypeSynonyms unsaturation check doesn't kick in
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.3
       Component:  Compiler (Type    |              Version:  8.6.2
  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 the
 [http://git.haskell.org/ghc.git/blob/984b75de7082689ebcc6e9d17b37f2c9b3702f71...
 first case] of `check_type`:

 {{{#!hs
 check_type env ctxt rank ty
   | not (null tvbs && null theta)
   = do  { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
         ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
                 -- Reject e.g. (Maybe (?x::Int => Int)),
                 -- with a decent error message

         ; check_valid_theta env' SigmaCtxt theta
                 -- Allow     type T = ?x::Int => Int -> Int
                 -- but not   type T = ?x::Int

         ; check_type env' ctxt rank tau      -- Allow foralls to right of
 arrow

         ; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
                    (forAllEscapeErr env' ty tau_kind)
         }
   where
     (tvbs, phi)  = tcSplitForAllVarBndrs ty
     (theta, tau) = tcSplitPhiTy phi

     tvs          = binderVars tvbs
     (env', _)    = tidyVarBndrs env tvs

     tau_kind              = typeKind tau
     phi_kind | null theta = tau_kind
              | otherwise  = liftedTypeKind
         -- If there are any constraints, the kind is *. (#11405)
 }}}

 In particular, this function uses `tcSplitForAllVarBndrs` and
 `tcSplitPhiTy` to decompose the right-hand side of a type synonym. What
 happens when that right-hand side is `B A` (from comment:1)? Well, as it
 happens, both `tcSplitForAllVarBndrs` and `tcSplitPhiTy` //expand type
 synonyms//, so `check_type` actually checks `forall x. x -> x` for
 validity, not `B A`! In other words, GHC is completely oblivious to the
 fact that `A` is unsaturated, since it's not checking the type `B A` in
 the first place.

 I suppose the prudent thing to do here would be to conjure up variations
 of `tcSplitForAllVarBndrs` and `tcSplitPhiTy` that don't expand type
 synonyms?

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15954#comment:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler