#14932 closed bug (fixed)

DeriveAnyClass produces unjustifiably untouchable unification variables

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.4.2
Component: Compiler (Type checker) Version: 8.4.1
Keywords: deriving Cc: kosmikus
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: deriving/should_compile/T14932
Blocked By: Blocking:
Related Tickets: #13272, #14933 Differential Rev(s): Phab:D4507
Wiki Page:

Description

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, 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.

Change History (8)

comment:1 Changed 18 months ago by RyanGlScott

Well, I do have a patch. But I also recently noticed the existence of #14933, which shares many similar characteristics with this issue, and now I'm wondering if perhaps I should clean up GHC's approach to DeriveAnyClass further to nail both bugs at once. Let me see how far I get...

comment:2 Changed 18 months ago by RyanGlScott

Differential Rev(s): Phab:D4507
Status: newpatch

comment:3 Changed 18 months ago by Ben Gamari <ben@…>

In 9893042/ghc:

Fix two pernicious bugs in DeriveAnyClass

The way GHC was handling `DeriveAnyClass` was subtly wrong
in two notable ways:

* In `inferConstraintsDAC`, we were //always// bumping the `TcLevel`
  of newly created unification variables, under the assumption that
  we would always place those unification variables inside an
  implication constraint. But #14932 showed precisely the scenario
  where we had `DeriveAnyClass` //without// any of the generated
  constraints being used inside an implication, which made GHC
  incorrectly believe the unification variables were untouchable.
* Even worse, we were using the generated unification variables from
  `inferConstraintsDAC` in every single iteration of `simplifyDeriv`.
  In #14933, however, we have a scenario where we fill in a
  unification variable with a skolem in one iteration, discard it,
  proceed on to another iteration, use the same unification variable
  (still filled in with the old skolem), and try to unify it with
  a //new// skolem! This results in an utter disaster.

The root of both these problems is `inferConstraintsDAC`. This patch
fixes the issue by no longer generating unification variables
directly in `inferConstraintsDAC`. Instead, we store the original
variables from a generic default type signature in `to_metas`, a new
field of `ThetaOrigin`, and in each iteration of `simplifyDeriv`, we
generate fresh meta tyvars (avoiding the second issue). Moreover,
this allows us to more carefully fine-tune the `TcLevel` under which
we create these meta tyvars, fixing the first issue.

Test Plan: make test TEST="T14932 T14933"

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14932, #14933

Differential Revision: https://phabricator.haskell.org/D4507

comment:4 Changed 18 months ago by bgamari

Milestone: 8.6.1

RyanGlScott, do you think this is ghc-8.4 material?

comment:5 Changed 18 months ago by RyanGlScott

I'm biased, but I think so. I'm amazed DeriveAnyClass was working correctly at all before this patch! (Plus, the patch looks larger than it really is—at its core, it's quite small.)

comment:6 Changed 18 months ago by Simon Peyton Jones <simonpj@…>

In 71d50db/ghc:

Minor refactor and commments

Minor refactor and comments, following Ryan's excellent DeriveAnyClass
bug (Trac #14932)

comment:7 Changed 18 months ago by RyanGlScott

Milestone: 8.6.18.4.2
Status: patchmerge
Test Case: deriving/should_compile/T14932

comment:8 Changed 18 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.