Opened 5 years ago

Closed 5 years ago

#4485 closed bug (fixed)

Per-class incoherence, and solve incoherent instances last

Reported by: JeremyShaw Owned by:
Priority: normal Milestone: 7.4.1
Component: Compiler Version: 7.0.1 RC1
Keywords: Cc: dsf@…, niklas.broberg@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: indexed-types/should_fail/T4485
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description (last modified by igloo)

The behavior of type-inference and OverlappingInstances has changed between GHC 6.12 and GHC 7.0 such that the following code type-checks under 6.12, but not 7.0rc2. I assume this change has something to do with the new type checker in GHC 7, but it is not clear to me if this change in behavior is intended. Nor am I clear how to achieve something similar to the old behavior. This is preventing HSP (and by extension, happstack) from migrating to GHC 7. I reported this earlier on the mailing lists, but I have further simplied the test case here.

> {-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FunctionalDependencies
>   , FlexibleContexts, FlexibleInstances, UndecidableInstances
>   , TypeSynonymInstances, GeneralizedNewtypeDeriving
>   , OverlappingInstances  
>   #-}
> module XMLGenerator where

XMLGenT monad transformer -- not really sure offhand why we have this, but we do:

> newtype XMLGenT m a = XMLGenT (m a)
>    deriving (Functor, Monad)

next we have a simple class for generating XML

> class Monad m => XMLGen m where
>  type XML m     -- ^ the type that will be used for the generated XML. Can be different on a per-monad basis
>  data Child m   -- ^ the type that will be used for children of an element
>  genElement :: String -> XMLGenT m (XML m) -- ^ a function to generate an element with no children or attributes. e.g. <br />

A class specifying how to turn a value of type 'c' into a list of Child elements

> class XMLGen m => EmbedAsChild m c where
>     asChild :: c -> XMLGenT m [Child m]

Next we have an instance of EmbedAsChild that embeds the XMLGenT wrapped 'c' value into 'm' by removing the XMLGenT wrapper, (implementation removed since it does not affect the error):

> instance (EmbedAsChild m c, m1 ~ m) => EmbedAsChild m (XMLGenT m1 c)

Now we have an instance which embeds 'XML' as a child. The specific type that is considered 'XML' is dependent on the XMLGen instance for 'm' (body also removed):

> instance (XMLGen m,  XML m ~ x) => EmbedAsChild m x

Next we define the Identity monad transformer and make it an instance of Monad and XMLGen:

> data Xml = Xml
> data IdentityT m a = IdentityT (m a)
> instance Monad (IdentityT m)
> instance XMLGen (IdentityT m) where
>     type XML (IdentityT m) = Xml

And we also define the Identity monad:

> data Identity a = Identity a
> instance Monad Identity

Here we specify a way to embed (XMLGenT Identity ()) into IdentityT IO:

> instance EmbedAsChild (IdentityT IO) (XMLGenT Identity ())

Next we define some arbitrary type that we want to convert to xml:

> data FooBar = FooBar

And now we try to create a more specific EmbedAsChild instance:

> instance EmbedAsChild (IdentityT IO) FooBar where
>   asChild b = asChild $ (genElement "foo")

Under GHC 6.12, everything type-checks fine. But under GHC 7 we get the error:

Prelude> :load "../XMLGenerator.lhs"                                                                                                                                                    
[1 of 1] Compiling XMLGenerator     ( ../XMLGenerator.lhs, interpreted )

../XMLGenerator.lhs:64:17:
    Overlapping instances for EmbedAsChild
				(IdentityT IO) (XMLGenT m (XML m))
      arising from a use of `asChild'
    Matching instances:
      instance [overlap ok] (m1 ~ m, EmbedAsChild m c) =>
                            EmbedAsChild m (XMLGenT m1 c)
	-- Defined at ../XMLGenerator.lhs:31:12-70
    (The choice depends on the instantiation of `m'
     To pick the first instance above, use -XIncoherentInstances
     when compiling the other instance declarations)
    In the expression: asChild
    In the expression: asChild $ (genElement "foo")
    In an equation for `asChild':
	asChild b = asChild $ (genElement "foo")
Failed, modules loaded: none.

I can make the error go away by specifying the type signature of genElement explicitly:

] instance EmbedAsChild (IdentityT IO) FooBar where
]   asChild b = asChild $ ((genElement "foo") :: XMLGenT (IdentityT IO) Xml)

But I would need to do this in dozens of places. (possibly hundreds). So that is not very pleasing.

Removing this instance also makes the error go away:

] instance EmbedAsChild (IdentityT IO) (XMLGenT Identity ())

But 'XMLGenT Identity ()' is not a type that genElement can have in that context.. Plus I need that instance..

Adding IncoherentInstances changes the error:

Prelude> :load "../XMLGenerator.lhs"                                                                                                                                                    
[1 of 1] Compiling XMLGenerator     ( ../XMLGenerator.lhs, interpreted )

../XMLGenerator.lhs:64:28:                                                                                                                                                              
    Couldn't match type `XMLGenT m (XML m)' with `Xml'
    In the second argument of `($)', namely `(genElement "foo")'
    In the expression: asChild $ (genElement "foo")
    In an equation for `asChild':
        asChild b = asChild $ (genElement "foo")
Failed, modules loaded: none.

I have attached a literate haskell version of this bug report that you can test with. Thanks!

Attachments (1)

XMLGenerator.lhs (5.0 KB) - added by JeremyShaw 5 years ago.
literate version of bug report which can be used as a test case

Download all attachments as: .zip

Change History (12)

Changed 5 years ago by JeremyShaw

literate version of bug report which can be used as a test case

comment:1 Changed 5 years ago by dsf

  • Cc dsf@… added

comment:2 Changed 5 years ago by simonpj

Thanks for the example. GHC 7 isn't behaving well here, but 6.12 may be behaving even worse.

Look at the typing problem that arises from

instance EmbedAsChild (IdentityT IO) FooBar where
   asChild b = asChild $ (genElement "foo")

After a bit of figuring, you should see that we have to solve the following type constraints:

     EmbedAsChild (IdentityT IO) (XMLGenT meta (XML meta)
     XMLGen meta

where meta is an unknown unification variable arising from instantiating the call to genElement :: XMLGen m => String -> XMLGenT m (XML m)`.

There are no other constraints on meta. OK, so now how is GHC supposed to figure out what meta is? Well, there are four instance declarations (each with a different context, but that doesn't matter here):

    EmbedAsChild (IdentityT IO) FooBar
    EmbedAsChild (IdentityT IO) (XMLGenT Identity ())
    EmbedAsChild m              (XMLGenT m1 c)
    EmbedAsChild m              x

Remember, we have to match without knowing what meta is going to turn out to be. The first cannot match, but the latter three in principle could, depending on how meta is eventually instantiated. The fourth is ignored becuase the third is more specific.

So there you are: we don't know which one to pick. In GHC 7 the error message is wrong, because it only mentions one of the two.

I'm honestly not sure why 6.12 accepts this.

So: what is your reasoning that says meta cannot instantite to Identity. Maybe you reason that XML Identity does not reduce to (), but that is very fragile. You might add such an instance declaration. And in any case it's beyond GHC's instance-matching powers to figure that out.

But perhaps you have an intutition in mind?

Simon

comment:3 Changed 5 years ago by nibro

  • Cc niklas.broberg@… added

The intended intuition is that whenever we come upon an unconstrained use of genElement, which produces some XMLGenT m1 (XML m1) where we can't resolve m1, but where we are within the context of some XMLGen m that we're embedding it in, default to m1 = m.

In other words, I would expect that the third alternative above defaulted to whenever we cannot actually infer that m1 = Identity.

Reading up on the documentation again, maybe this is exactly what IncoherentInstances does after all? What worries me is that IncoherentInstances might cause the third alternative to be chosen "too early", but maybe that's just superstition.

comment:4 Changed 5 years ago by simonpj

Right. I think you need IncoherentInstances. With this flag, and the new typechecker patches, your module compiles ok.

Currently GHC crashes without IncoherentInstances, for a tiresome reason; Dimitrios is fixing that.

To make IncoherentInstances behave as well as possible, we should really wait until all other equalities are solved, to minimise the chance of a bogus choice (as you say). We'll do that in due course.

Simon

comment:5 Changed 5 years ago by JeremyShaw

Regarding, XMLGenT Identity (), I just meant that:

instance EmbedAsChild (IdentityT IO) FooBar where
   asChild b = asChild $ ((genElement "foo") :: XMLGenT Identity ())

produces a type error. So clearly genElement does not actually have that type. But I make no informed claims that the GHC type checker should be able to figure that out.

Your explanation makes sense (and matches what is in the documentation). The fact that things worked under GHC 6.12, made me wonder if there was some other secret voodoo that I did not know about, or if 6.12 was just conveniently broken.

I am a little bit frightened of enabling IncohorentInstances. If they could be enabled just in the original module where the class is enabled, that might not be so bad. But if I have to enabled them everywhere I used the class, that is not so thrilling. In my experience, enabling IncohorentInstances is almost never the right thing to do. Since I use other classes and instances, it would also allow those to be incoherent when I would really prefer a compiler error.

It would be somewhat nice if IncoherentInstances could be enabled on a per-class basis due to its 'unsafe' nature.

thanks!

  • jeremy

comment:6 Changed 5 years ago by igloo

  • Description modified (diff)

comment:7 Changed 5 years ago by igloo

  • Milestone set to 7.2.1

comment:8 Changed 5 years ago by simonpj

  • Summary changed from Unexplained change in type-inference + OverlappingInstances in to Per-class incoherence, and solve incoherent instances last

This patch fixes the crash in overlap reporting. Please push to the 7.0 branch.

Mon Nov 15 14:28:05 GMT 2010  [email protected]
  * Ensure that instance overlap errors are report properly
  
  This (annoyingly) requires us to re-flatten the class predicate.
  See Note [Flattening in error message generation]

    M ./compiler/typecheck/TcErrors.lhs -37 +91

I'll re-title the ticket to now ask for per-class incoherent instances (which is a feature that makes sense to me). This links to people who want somewhat less draconian checking on instance overlap: #3877 and #4259.

Also there's a case for making the solver solve (incoherent) type class instances last, so that all the equality info we have is available.

Simon

comment:9 Changed 5 years ago by simonpj

  • Test Case set to indexed-types/should_fail/T4485

Added a regression test for the instance-overlap crash.

comment:10 Changed 5 years ago by igloo

Merged.

comment:11 Changed 5 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed

I've just checked. Both "overlapping-intsances" and "incoherent-instances" are recorded for the instance declaration; what matters is what flags were on when the instance decls were compiled, not when the instances are used. The documentation seems to reflect that.

When I said I'd leave the ticket open for "per-clas incoherent instances" I really meant "per-instance" and we have that. (Or at least, recorded per-instance, albeit from a per-module flag. A more local pragma would also make sense, but that's a separate feature.)

So I'll close this ticket.

Note: See TracTickets for help on using tickets.