Opened 3 years ago

Closed 3 years ago

#10195 closed bug (fixed)

GHC forgets constraints when matching on GADTs

Reported by: crockeea Owned by:
Priority: normal Milestone: 7.10.2
Component: Compiler Version: 7.8.4
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T10195
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by crockeea)

Here's a relatively short piece of code that doesn't compile:

{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, GADTs, 
             ConstraintKinds, KindSignatures,
             FlexibleInstances #-}

module Foo where

import GHC.Exts

data Foo m zp r'q = Foo zp
data Dict :: Constraint -> * where
  Dict :: a => Dict a

type family BarFamily a b :: Bool
class Bar m m'
instance (BarFamily m m' ~ 'True) => Bar m m'

magic :: (Bar m m') => c m zp -> Foo m zp (c m' zq)
magic = undefined
getDict :: a -> Dict (Num a)
getDict _ = undefined
fromScalar :: r -> c m r
fromScalar = undefined

foo :: (Bar m m')
  => c m zp -> Foo m zp (c m' zq) -> Foo m zp (c m' zq)
foo b (Foo sc) = 
  let scinv = fromScalar sc
  in case getDict scinv of
    Dict -> magic $ scinv * b

GHC complains that it cannot deduce (BarFamily m m' ~ 'True) arising from a use of `magic` in the definition of foo. Of course this is silly: magic requires Bar m m', which is supplied as a constraint to foo. So GHC is forgetting about the constraint on foo and instead trying to satisfy the generic instance of Bar which has the constraint (BarFamily m m' ~ 'True).

I've found no less than six different ways to poke this code to make it compile, and some of them seem to reveal dangerous/unexpected behavior. The following are all deltas from the original code above and result in compiling code.

  1. Add ScopedTypeVariables and give scinv an explicit signature: let scinv = fromScalar sc :: c m z in ... I'm not sure why this would make GHC suddenly realize that it already has the constraint Bar m m', but it seems to. (What it definitely does *not* do is result in a BarFamily m m' ~ 'True constraint.)
  1. Remove the instance for Bar. This seems highly suspicious: the presence (or lack thereof) of an instance changes how GHC resolves the constraint in foo.
  1. Change the constraint on foo to BarFamily m m' ~ 'True. In this case, GHC does *not* forget the constraint on foo and successfully uses it to satisfy the instance of Bar. Why does GHC forget about Bar m m' but not BarFamily m m' ~ 'True?
  1. Add the superclass constraint BarFamily m m' ~ 'True to class Bar. Adding this constraint either makes GHC find the Bar m m' constraint on foo or, even more bizarrely, GHC still forgets about Bar m m' but manages to get the superclass constraint from Bar m m' and uses it to satisfy the instance.
  1. Add PolyKinds. Not sure why this would affect anything.
  1. Change the signature of fromScalar to r -> s. Not sure why this would affect anything.

Change History (11)

comment:1 Changed 3 years ago by rwbarton

I'm no expert on this part of the compiler, but it looks like GHC reduces the wanted constraint Bar m m' (from the use of magic) to BarFamily m m' ~ 'True (because of the Bar instance), and then it can no longer deduce that from Bar m m'. A peculiar scenario.

It certainly looks wrong though, and FWIW GHC 7.6.3 accepts the program.

The robust workaround is to add the superclass constraint BarFamily m m' ~ 'True to Bar m m', since then (as you describe as "even more bizarrely") GHC can deduce either of BarFamily m m' ~ 'True and Bar m m' from the other, and then can't get stuck in this kind of situation.

comment:2 Changed 3 years ago by crockeea

Can you confirm in 7.10?

Since we have no idea what's causing the issue, nor exactly what "this situation" is, it's possible this behavior could occur for a less generic instance in a situation where the instance constraint can't just be trivially promoted to a superclass constraint.

comment:3 Changed 3 years ago by rwbarton

Yes, the original program fails to compile in 7.8.1, 7.10-rc-something, and HEAD, though I didn't try your variations to see if they have the same behavior also.

comment:4 Changed 3 years ago by goldfire

Interesting.

One problem with this code is that it sports some overlapping instances. Your local Bar m m' constraint overlaps with the global Bar m m' instance. It's not terribly surprising to me that GHC gets confused here. This is a dark corner of FlexibleInstances.

Part of the problem is that it's hard for GHC to know what the type of magic $ scinv * b should be. Due to the GADT pattern-match, it doesn't want to guess that the type should be Foo m zp (c m' zq), as that choice might be ignoring some information gained in the pattern-match. My guess is that some of your deltas cause GHC to deduce that no equalities are learned in the pattern-match, and thus that result type inference is safe.

In any case, I don't think GHC is "forgetting" anything here. It's just choosing one seemingly-viable route toward a solution (the global instance) instead of another, the local constraint. I do agree that this behavior is somewhat disconcerting, though.

comment:5 Changed 3 years ago by crockeea

goldfire: In what sense does the Bar m m' constraint overlap with the instance? As far as I was aware, the definition of an overlapping instance requires *two* instances whose RHS matches a given constraint. Thus it would be impossible to have "overlapping" instances with just a single instance. This is likely just a misunderstanding of the term on my part.

Last edited 3 years ago by crockeea (previous) (diff)

comment:6 Changed 3 years ago by goldfire

I'm perhaps abusing the term "overlap". What I mean here is that GHC has two routes with which to satisfy a Bar m m' constraint. Let's rename variables in the global instance for clarity: instance (BarFamily b b' ~ 'True) => Bar b b'. During type inference, GHC has to solve a Bar p q constraint, for some p and some q. If, at this point during inference, it knows p ~ m and q ~ m', GHC will prefer the local constraint Bar m m'. Otherwise, if we don't yet know enough about p and q, it will use the global instance and then require BarFamily p q ~ 'True. Even if we later learn that p ~ m and q ~ m', it's too late to use the Bar m m' constraint.

I do know that GHC "tries hard" to resolve equality constraints before class constraints, but guaranteeing that this happens may be impossible. So, you'll end up with situations like these.

I'd be quite curious for Simon's input here. He's on holiday at the moment, but I'm sure he'll chime in ere too long.

comment:7 Changed 3 years ago by crockeea

Description: modified (diff)

comment:8 Changed 3 years ago by simonpj

I understand what is going on here. We get this constraint from the call to magic:

forall[2] c m m' zp. Bar m m' =>
   forall[3]. Num (c m zp) => 
     Bar meta[2] m', meta[2]~m

The [2] and [3] are the "untouchable" levels, and meta[2] is a level-2 unification variable. When checking whether we can safely fire the top-level instance (Bar b b'), we try to unify the given Bar m m' with Bar meta[2] m'. The unification variable meta[2] is untouchable, so we wrongly made it behave like a skolem in this unification, so the unification failed, and so we fired the top-level instance.

But the (meta[2] ~ m) constraint, if allowed to float out and then fire, will make the Bar meta[2] m' turn into Bar m m', which can then be discharged by the given Bar m m'.

So the mistake here is being a bit too eager when asking "is the top-level instance the only one that could apply?". The fix is easy. But of course it means that fewer top-level instances will fire, so it's possible that it will break other examples that currently "work". But rightly so, I think.

comment:9 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 8b7ceece52d2a0bb8a4ea5609da286fb76d88211/ghc:

More aggressive Given/Wanted overlap check

This fixes Trac #10195

For some reason we considered untouchability before, but Trac #10195
shows that this is positively worng.

See Note [Instance and Given overlap] in TcInteract.

Looking at the Git log, it seems that this bug was introduced at the
same time that we introduced the Given/Wanted overlap check in the first
place.

comment:10 Changed 3 years ago by simonpj

Milestone: 7.10.2
Status: newmerge
Test Case: typecheck/should_compile/T10195

Very good! Fixed.

This is worth merging.

Simon

comment:11 Changed 3 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Merged to ghc-7.10.

Note: See TracTickets for help on using tickets.