Opened 4 years ago

Closed 15 months ago

#11282 closed bug (duplicate)

Error warns about non-injectivity of injective type family

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.11
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: #14369 Differential Rev(s):
Wiki Page:

Description (last modified by goldfire)

When I say

{-# LANGUAGE TypeFamilies, RankNTypes #-}

module Bug where

import GHC.Exts

type family F a = r | r -> a
type family G a :: Constraint

meth :: (G a => F a) -> ()
meth = undefined

I get

Bug.hs:10:9: error:
    • Could not deduce: F a ~ F a0
      from the context: G a0
        bound by the type signature for:
                   meth :: G a0 => F a0
        at Bug.hs:10:9-26
      NB: ‘F’ is a type function, and may not be injective
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘meth’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        meth :: (G a => F a) -> ()

The presence of G a is critical for exhibiting this bug. If I replace G a with Show a the problem disappears.

This one was actually encountered in an attempt to do Useful Work, not just idle typecheckery.

EDIT: Actually, I understand why this program should be rejected (comment:1), but the error message is surely misleading and should be fixed.

Change History (6)

comment:1 Changed 4 years ago by goldfire

Actually, this has nothing to do with injective type families. If I change the code to

meth :: (G a => a) -> ()

I get an error. That error explains that a is untouchable, which makes some small degree of sense, given that G a might reduce to an equality constraint.

But the original error message is quite unfortunate, because F is indeed injective!

So this bug is really about the error message, not the rejection.

comment:2 Changed 4 years ago by simonpj

Yes, this is unfortunate. Here's a bit more detail.

The ambiguity check does a subsumption check

  forall a. (G a => F a) -> ()   <=    forall b. (G b => F b) -> ()

So we skolemise b and instantiate b to beta:

  forall a. (   (G a => F a) -> ()   <=    (G beta => F beta) -> ()  )

Now we do co/contravariance (see Note [Co/contra-variance of subsumption checking] in TcUnify) to get

  forall a.  (G beta => F beta)   <=    (G a -> F a)

Now we skolemise and instantiate again (in this case there are no foralls, but we still get an implication constraint:

  forall a.   (forall. G beta =>   (F a ~ F beta))

Now as you point out beta is untouchable, and we can't float out the equality because G beta might have equalities in it. Alas.

I'm not sure what to do about this. But that's what's happening.

comment:3 Changed 4 years ago by goldfire

Description: modified (diff)
Summary: Injectivity annotation fails in the presence of higher-rank use of constraint familyError warns about non-injectivity of injective type family

I had figured that out (in rather less detail) by looking at the case without the injective type family. But the original error message is still warning me about a type family that isn't injective! So I think this boils down to adding a bit more logic to TcErrors to print out an error about untouchable variables here instead of non-injective type families.

I've modified the title and description to make this more clear.

comment:4 Changed 4 years ago by thomie

Type of failure: None/UnknownIncorrect warning at compile-time

comment:5 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:6 Changed 15 months ago by RyanGlScott

Resolution: duplicate
Status: newclosed

Closing as a duplicate of #14369. After commit 8846a7fdcf2060dd37e66b4d1f89bd8fdfad4620 (which fixed #14369), the error message no longer claims that F may not be injective:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs -XTypeFamilyDependencies
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:10:9: error:
    • Could not deduce: F a ~ F a0
      from the context: G a0
        bound by the type signature for:
                   meth :: G a0 => F a0
        at Bug.hs:10:9-26
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘meth’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: meth :: (G a => F a) -> ()
   |
10 | meth :: (G a => F a) -> ()
   |         ^^^^^^^^^^^^^^^^^^
Note: See TracTickets for help on using tickets.