Opened 5 years ago

Closed 4 years ago

Last modified 4 years ago

#10009 closed bug (fixed)

type inference regression when faking injective type families

Reported by: aavogt Owned by:
Priority: highest Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.10.1-rc1
Keywords: Cc: adamgundry, kosmikus, goldfire, jeltsch, Lemming
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T10009
Blocked By: Blocking:
Related Tickets: #10226, #10634 Differential Rev(s):
Wiki Page:

Description

ghc-7.10.0.20141222 does not accept the program unless I uncomment the type signature (a :: a). ghc-7.8 accepts it as-is.

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

class (UnF (F a) ~ a, Show a) => C a where
    type F a
    f :: F a -> a

type family UnF a

g :: forall a. C a => a -> String
g _ = show a
  where a = f (undefined :: F a) -- :: a

Change History (43)

comment:1 Changed 5 years ago by dfeuer

Component: CompilerCompiler (Type checker)
Milestone: 7.10.1
Priority: normalhigh
Type of failure: None/UnknownGHC rejects valid program

Setting high priority because this is (apparently) a regression. If the powers that be think it should be this way, then they can of course close the ticket.

comment:2 Changed 5 years ago by dfeuer

Resolution: worksforme
Status: newclosed

I just tested with 7.11.20150103 and I couldn't reproduce the problem. I tried

  where a = f (undefined :: F a) :: a
  where a :: a = f (undefined :: F a)
     --and also
  where a :: a
        a = f (undefined :: F a)

so unless there's some code missing from this example, it's been fixed.

comment:3 Changed 5 years ago by rwbarton

Resolution: worksforme
Status: closednew

Did you try the original program in the ticket? I get an error with 7.11.20150112.

comment:4 in reply to:  3 Changed 5 years ago by dfeuer

Replying to rwbarton:

Did you try the original program in the ticket? I get an error with 7.11.20150112.

I misread; sorry! I thought the problem was when it was uncommented.

comment:5 Changed 5 years ago by simonpj

This is a bug. Excellent but report, thank you Adam.

Happily I've fixed it. I'm tied up the next day or two, but I'll commit by Thurs night.

Simon

comment:6 Changed 5 years ago by simonpj

I was wrong. I have not fixed it, only a simpler version of it. So I'm not going to get this done this week after all.

Austin: go ahead and make RC2, don't wait for this.

  • It affects very little code;
  • It can always be fixed by adding a type signature

I believe that HList is the main affected library. What I don't know is whether it affects the library itself or clients of the library.

Simon

comment:7 Changed 5 years ago by aavogt

It affects both: the library has a number of definitions that don't compile with 7.10RC1 right now. It affects how clients can put library functions together. For example the library defines:

-- possible type signatures:
-- hUntagSelf :: HList '[Tagged x x, Tagged y y] -> HList '[x,y]
-- hTagSelf   :: HList '[x,y] -> HList '[Tagged x x, Tagged y y]

-- hZipTIP :: TIP '[Tagged x x] -> TIP '[Tagged y y]
--                 -> TIP '[Tagged (x,y) (x,y)]
hZipTIP (TIP x) (TIP y) = TIP (hTagSelf (hZipList (hUntagSelf x) (hUntagSelf y)))

If I figure out where to annotate to get rid of the 7.10RC1 type error:

Data/HList/TIP.hs:251:1: Warning:
    Could not deduce (TagR a0 ~ TagR a)
    from the context (HZipList x y a,
                      TagUntag a,
                      TagUntag x,
                      TagUntag y)
      bound by the inferred type for ‘hZipTIP’:
                 (HZipList x y a, TagUntag a, TagUntag x, TagUntag y) =>
                 TIP (TagR x) -> TIP (TagR y) -> TIP (TagR a)
      at Data/HList/TIP.hs:251:1-81
    NB: ‘TagR’ is a type function, and may not be injective
    The type variable ‘a0’ is ambiguous
    Expected type: TIP (TagR x) -> TIP (TagR y) -> TIP (TagR a)
      Actual type: TIP (TagR x0) -> TIP (TagR y0) -> TIP (TagR a0)
    When checking that ‘hZipTIP’ has the inferred type
      hZipTIP :: forall (a :: [*]) (x :: [*]) (y :: [*]).
                 (HZipList x y a, TagUntag a, TagUntag x, TagUntag y) =>
                 TIP (TagR x) -> TIP (TagR y) -> TIP (TagR a)
    Probable cause: the inferred type is ambiguous

Data/HList/TIP.hs:251:1: Warning:
    Could not deduce (HZipList x0 y0 a0)
    from the context (HZipList x y a,
                      TagUntag a,
                      TagUntag x,
                      TagUntag y)
      bound by the inferred type for ‘hZipTIP’:
                 (HZipList x y a, TagUntag a, TagUntag x, TagUntag y) =>
                 TIP (TagR x) -> TIP (TagR y) -> TIP (TagR a)
      at Data/HList/TIP.hs:251:1-81
    The type variables ‘a0’, ‘x0’, ‘y0’ are ambiguous
    When checking that ‘hZipTIP’ has the inferred type
      hZipTIP :: forall (a :: [*]) (x :: [*]) (y :: [*]).
                 (HZipList x y a, TagUntag a, TagUntag x, TagUntag y) =>
                 TIP (TagR x) -> TIP (TagR y) -> TIP (TagR a)
    Probable cause: the inferred type is ambiguous

clients probably want to define functions like this too, and requiring a type annotation here probably doubles the amount of code that has to be written.

comment:8 Changed 5 years ago by aavogt

for what it's worth, ghc-7.10RC1 handles FDs correctly (see http://stackoverflow.com/questions/24110410/type-families-get-stuck-where-the-equivalent-type-using-functional-dependencies), as well as MPTCs+TFs so long as f doesn't use the TFs directly:

class (b ~ GetB a, a ~ GetA b, Show a) => C b a where
    type GetB a
    type GetA b
    f :: b -> a
    -- f :: GetB a -> a -- but not this one!

g :: forall a b. C b a => a -> String
g _ = show a
  where a = f (undefined :: GetB a) -- :: a

comment:9 Changed 5 years ago by simonpj

Thank you for clarifying; most helpful.

I'm sorry but Austin is cutting RC2 today and I can't fix this late-reported regression in time. I will try to get it done before the final release comes out.

Last edited 5 years ago by simonpj (previous) (diff)

comment:10 Changed 5 years ago by darchon

7.10-RC3 was just released, but this bug is still not fixed. Is the fix in HEAD? Will it be fixed in 7.10.1?

comment:11 Changed 5 years ago by simonpj

Rats. I wish you'd highlighted this earlier. We've been advertising 7.10.1 for ages, with a clearly stated list of priorities on the 7.10.1 status page. It says that we'll only fix "highest" priority bugs. If you care deeply about things, it's a good idea to monitor the status page and bid to have it promoted to "highest".

I'm not sure how to proceed now. I don't know how hard it is to fix. I don't know how mission-critical it is to how many people. More info on the latter would be helpful.

Simon

comment:12 Changed 5 years ago by darchon

It is not mission critical for me. I just encountered a piece of code of my own that works on 7.8.4, but complains (perhaps rightfully so) about ambiguous types in 7.10.1-rc3. I just got a hit on this issue when googling the error message, and my question was merely if a fix in HEAD slipped through, and did not make it in 7.10.1-rc3.

Christiaan

Last edited 5 years ago by darchon (previous) (diff)

comment:13 Changed 5 years ago by simonpj

OK good, thanks! (And that accounts for why you didn't yell.) Let's see if it's mission critical for anyone else.

comment:14 Changed 5 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone.

comment:15 Changed 5 years ago by jstolarek

comment:16 Changed 5 years ago by adamgundry

Cc: adamgundry added

comment:17 Changed 5 years ago by edsko

Reported this independently, didn't see this ticket, sorry. But we were just bitten by this in ide-backend as well (we can work around it with proxies). See https://ghc.haskell.org/trac/ghc/ticket/10226 for an independent example, might perhaps be useful as a second test case (and some detailed comments there as well). Note that I do *not* think, as per @simonpj 's comment above, that "It can always be fixed by adding a type signature".

comment:18 Changed 5 years ago by kosmikus

Cc: kosmikus added

comment:19 Changed 5 years ago by simonpj

Cc: goldfire added

comment:20 Changed 5 years ago by adamgundry

Milestone: 7.12.17.10.2

Any chance we can get this addressed for 7.10.2? It's a definite failure of completeness in the constraint solver that is a regression from 7.8 and is affecting code in the wild. It is possible to rewrite affected code using proxies, but only with fairly invasive changes. As Edsko noted, adding type signatures is not necessarily enough.

comment:21 Changed 5 years ago by simonpj

Thanks for re-highlighting this. I've just been looking at this again, as it happens.

The sad story is that it's an unexpected consequence of some refactoring I did to the type-family solver. I can't undo that on the branch; it's quite pervasive. But it showed up a shortcoming in the way we do type inference generally. That is, I exposed an existing bug which happened not to show up before. Fixing that bug is quite non-trivial.

I do intend to fix it, probably in the next couple of weeks. Let's see how invasive the fix is.

Meanwhile you say "it is affecting code in the wild". Can you be more specific?

Simon

comment:22 Changed 4 years ago by Simon Peyton Jones <simonpj@…>

In a1275a762ec04c1159ae37199b1c8f998a5c5499/ghc:

Improve improvement in the constraint solver

This regrettably-big patch substantially improves the way in which
"improvement" happens in the constraint solver.  It was triggered by
trying to crack Trac #10009, but it turned out to solve #10340 as
well.

The big picture, with several of the trickiest examples, is described
in Note [The improvement story] in TcInteract.

The major change is this:

* After solving we explicitly try "improvement", by
     - making the unsolved Wanteds into Deriveds
     - allowing Deriveds to rewrite Deriveds
  This more aggressive rewriting "unlocks" some extra
  guess-free unifications.

* The main loop is in TcInteract.solveSimpleWanteds, but I also ended
  up refactoring TcSimplify.simpl_loop, and its surrounding code.

  Notably, any insolubles from the Givens are pulled out
  and treated separately, rather than staying in the inert set
  during the solveSimpleWanteds loop.

There are a lot of follow-on changes

* Do not emit generate Derived improvements from Wanteds.
  This saves work in the common case where they aren't needed.

* For improvement we should really do type-class reduction on Derived
  constraints in doTopReactDict.  That entailed changing the GenInst
  constructor a bit; a local and minor change

* Some annoying faffing about with dropping derived constraints;
  see dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
  and their Notes.

* Some substantial refactoring in TcErrors.reportWanteds.
  This work wasn't strictly forced, but I got sucked into it.
  All the changes are in TcErrors.

* Use TcS.unifyTyVar consistently, rather than setWantedTyBind,
  so that unifications are properly tracked.

* Refactoring around solveWantedsTcM, solveWantedsAndDrop.
  They previously guaranteed a zonked result, but it's more
  straightforward for clients to zonk.

comment:23 Changed 4 years ago by Simon Peyton Jones <simonpj@…>

In d4a926ba52fbbbdeaadfff7c86e7175c8cc1b97c/ghc:

Test Trac #10226

Fixed by the patch for #10009

comment:24 Changed 4 years ago by simonpj

Phew! That was far more work than I expected.

It's not clear whether to merge this to 7.10

  • It probably won't merge cleanly; but we can probably deal with that if necessary
  • It's a big patch, so there's always a risk of messing something else up

It fixes: #10009, #10226, #10340.

Opinions?

Simon

comment:25 Changed 4 years ago by simonpj

I tried to test hlist-0.3.4.1, but stalled on

Data/HList/HList.hs:55:1:
    The associated type ‘UnPrime’
    mentions none of the type or kind variables of the class ‘ConvHList a’
    In the class declaration for ‘ConvHList’

which is an absolutely correct error message.

Simon

comment:26 Changed 4 years ago by kosmikus

First of all, thanks a lot, Simon.

I'll try to build HEAD soon and see if I can test this.

I would obviously like this to be merged into 7.10, because the bugs triggered by this, while seemingly exotic, are still regressions. And 7.12 is probably a long time away ...

comment:27 Changed 4 years ago by kosmikus

Re hlist: I'm surprised this ever worked. What I usually do is to define the UnPrime-equivalent outside of the class (as a type family), and Prime within. I hadn't considered that there may have been GHC versions that would have allowed both to be defined within the class.

comment:28 Changed 4 years ago by simonpj

I'm surprised too; presumably a bug in earlier GHC's let it sneak through

comment:29 Changed 4 years ago by jeltsch

I have an issue with GHC 7.10.1, which is probably rooted in the same bug. The following code is accepted by GHC 7.8.3, but not 7.10.1:

{-# LANGUAGE TypeFamilies #-}

type family F a :: *

type family G b :: *

x :: G (F a) ~ a => F a
x = undefined

GHC 7.10.1 gives the following error message:

Could not deduce (F a0 ~ F a)
from the context (G (F a) ~ a)
  bound by the type signature for x :: (G (F a) ~ a) => F a
  at Test.hs:7:6-23
NB: ‘F’ is a type function, and may not be injective
The type variable ‘a0’ is ambiguous
In the ambiguity check for the type signature for ‘x’:
  x :: forall a. (G (F a) ~ a) => F a
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘x’: x :: G (F a) ~ a => F a

Is this code accepted by GHC HEAD?

I came across this problem when trying to recompile the incremental-computing package with GHC 7.10.1. Since this issue breaks incremental-computing in a nontrivial way, I would be extremely happy if the fix of this bug would make it into GHC 7.10.2.

comment:30 Changed 4 years ago by jeltsch

Cc: jeltsch added

comment:31 in reply to:  29 Changed 4 years ago by rwbarton

Replying to jeltsch:

Is this code accepted by GHC HEAD?

Yes, though it also gives a warning about a redundant constraint G (F a) ~ a...

comment:32 Changed 4 years ago by simonpj

Priority: highhighest
Status: newmerge

Let's see if Austin can merge that big patch in comment:22 to 7.10.2, if that does actually fix the problems you are having.

That said, I'm not finished with this ticket. I had to park it for a while, but I know that the solution is incomplete and am working on making it better. So please don't close the ticket after merging: put it back to 'new' with 7.12 milestone.

Still, I think the above patch is a big improvement.

Simon

Last edited 4 years ago by simonpj (previous) (diff)

comment:33 Changed 4 years ago by Simon Peyton Jones <simonpj@…>

In ddbb97d00fdbc5870a4076ed15af8e607b161cb2/ghc:

Another major improvement of "improvement"

I wasn't very happy with my fix to Trac #10009. This is much better.

The main idea is that the inert set now contains a "model", which
embodies *all* the (nominal) equalities that we know about, with
a view to exposing unifications.  This requires a lot fewer iterations
of the solver than before.

There are extensive comments in
 TcSMonad:  Note [inert_model: the inert model]
            Note [Adding an inert canonical constraint the InertCans]

The big changes are

  * New inert_model field in InertCans

  * Functions addInertEq, addInertCan deal with adding a
    constraint, maintaining the model

  * A nice improvement is that unification variables can
    unify with fmvs, so that from, say   alpha ~ fmv
    we get              alpha := fmv
    See Note [Orientation of equalities with fmvs] in TcFlatten
    It's still not perfect, as the Note explains

New flag -fconstraint-solver-iterations=n, allows us to control
the number of constraint solver iterations, and in particular
will flag up when it's more than a small number.

Performance is generally slightly better:
T5837 is a lot better for some reason.

comment:34 Changed 4 years ago by jeltsch

Thank you very much, Simon. I think I will test this new solution with incremental-computing soon.

Is there any chance that this patch or the previous one will make it into GHC 7.10.2?

comment:35 Changed 4 years ago by simonpj

Is there any chance that this patch or the previous one will make it into GHC 7.10.2?

coment:33 won't. I hope that comment:22 will (Austin is working on exactly that). According to comment:21, it's to be enough to solve your problem.

comment:36 Changed 4 years ago by thoughtpolice

Milestone: 7.10.27.12.1
Resolution: fixed
Status: mergeclosed

Sigh, so unfortunately I've spent some more time futzing around with the patch, and I just don't think it can be merged in a sensible way without even more work. And even though the work seems doable I'm just very averse to the risk of it at this point, I'm afraid. I think I've even got the redundant superclass constraint patch building, but I'm just not sure it's worth it.

This is most certainly a regression but realistically I'm not sure how much it will come up. There have been three users who want it (Adam, Adam and Wolfgang) and who have reported it as "please fix" AFAICS, but as Simon originally said it shouldn't affect much code, and we didn't hold the original release up for this bug anyway.

Unless there is overwhelming evidence this is a common and game breaking bug that has cropped up in practice (which I'm really not sure of!), I've decided to leave this out of the release candidate, and subsequently, the final release.

Wolfgang, I sincerely apologize for this as it is not an easy thing for you to work around in your paper or library, and I understand it's suboptimal (and even frustrating). But I would rather ship the significant improvements we have now for even more users to make things better. I'm sorry this one missed the boat.

FTR, I tried merging in the redundant superclass constraints patch (since the improvement patch was dependent on it), which on its own has actually proved to be a bit difficult. But I'm just getting more risk aversive to this - these patches also have tons of knock on changes like error messages (which are merely a hassle), but even worse, further bugfixes of their own in more patches later - which I'd have to track, adopt and make sure are fixed. And even then, _none_ of these patches are in a released compiler - there's been churn here from Simon recently. It's not clear when to _stop_.

So it's impossible to tell if I should pick up *just* that patch, or that patch + 10 others because the intermediate states are all variously broken, or that patch + the next 5 'bugfix + refactor' patches are good enough. Once I've pushed these two, I'm just not sure how *many more* I'll have to push.

So I'm moving this to 7.12.1 and closing it. Simon, please re-open if you think there's more work to be done here. Again, I apologize for the lead-on with this one, but after getting closer and closer, it simply does not seem worth it I'm afraid.

comment:37 Changed 4 years ago by simonpj

I'm afraid Austin is right. It's an area I've been working on hard recently, so short of picking up the current state of play (which would would introduce a lot of new risk to the 7.10 branch, including perhaps API changes) there isn't a lot we can do.

Simon

comment:38 Changed 4 years ago by jstolarek

comment:39 Changed 4 years ago by Lemming

I was hit by this bug in hmm-hmatrix but I remember that I used this pattern in more places. Originally I added the equality constraint because I wanted to avoid type annotations. Thus adding type signatures at the call sites is contrary to my initial goal. An option would be to replace the single-parameter type class by a multi-parameter one, thus giving the result of F a a type variable name.

I added #10634, which however is much abstracted from the original code.

Last edited 4 years ago by Lemming (previous) (diff)

comment:40 Changed 4 years ago by Lemming

Cc: Lemming added

comment:41 in reply to:  27 Changed 4 years ago by Lemming

Replying to kosmikus:

Re hlist: I'm surprised this ever worked. What I usually do is to define the UnPrime-equivalent outside of the class (as a type family), and Prime within. I hadn't considered that there may have been GHC versions that would have allowed both to be defined within the class.

I used that technique several times after I found out that it worked. I expected that GHC knows what it does. :-) I am now reverting the affected definitions.

comment:42 Changed 4 years ago by simonpj

Test Case: typecheck/should_compile/T10009

comment:43 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

Note: See TracTickets for help on using tickets.