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:1114
• 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 genericssop
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 