DeriveAnyClass produces unjustifiably untouchable unification variables

The following code (courtesy of kosmikus) should typecheck, but does not:

{-# 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 (closed), 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 example.

Patch incoming.

Trac metadata

Trac field	Value
Version	8.4.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related	#13272 (closed)
Blocking
CC	kosmikus
Operating system
Architecture