[GHC] #14932: DeriveAnyClass produces unjustifiably untouchable unification variables

[GHC]

#14932: DeriveAnyClass produces unjustifiably untouchable unification variables
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.4.1
  (Type checker)                     |
           Keywords:  deriving       |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #13272
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following code (courtesy of kosmikus) should typecheck, but does not:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 module Zero where

 import GHC.Exts

 class Zero a where
  zero :: a
  default zero :: (Code a ~ '[xs], All Zero xs) => a
  zero = undefined

 type family All c xs :: Constraint where
  All c '[] = ()
  All c (x : xs) = (c x, All c xs)

 type family Code (a :: *) :: [[*]]
 type instance Code B1 = '[ '[ ] ]

 data B1 = B1
  deriving Zero
 }}}

 This produces the following error:

 {{{
 GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /nfs/nfs7/home/rgscott/.ghci
 [1 of 1] Compiling Zero             ( Bug.hs, interpreted )

 Bug.hs:23:11: error:
     • Couldn't match type ‘xs0’ with ‘'[]’
         arising from the 'deriving' clause of a data type declaration
         ‘xs0’ is untouchable
           inside the constraints: All Zero xs0
           bound by the deriving clause for ‘Zero B1’
           at Bug.hs:23:11-14
     • When deriving the instance for (Zero B1)
    |
 23 |  deriving Zero
    |           ^^^^
 }}}

 This error is baffling, however, because `xs0` should be a unification
 variable that readily unifies with `'[]`! As evidence, this typechecks:

 {{{
 instance Zero B1
 }}}

 But the equivalent `deriving` clause does not.

 I know what is going on here after some sleuthing: `DeriveAnyClass`
 (specifically, `inferConstraintsDAC`) is producing unification variables
 whose TcLevel is always bumped to three. However, in the program above, we
 will not form an implication constraints around those unification
 variables, since `zero` has no locally quantified type variables or given
 constraints. Thus, `simplifyDeriv` will try to simplify unification
 variables with TcLevel 3 at the top level, which results in them being
 untouchable. Blegh.

 This was partially noticed in #13272, when we were failing to bump
 unification variables that //did// appear inside implication constraints.
 However, we overlooked this one corner case, which kosmikus happened to
 stumble upon in a `generics-sop`
 [https://stackoverflow.com/a/49335338/1482749 example].

 Patch incoming.

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