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 |