[GHC] #10675: GHC does not check the functional dependency consistency condition correctly

[GHC]

#10675: GHC does not check the functional dependency consistency condition
correctly
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.1
      Resolution:                    |             Keywords:  FunDeps
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 Replying to [comment:15 simonpj]:  On the broader issue of should those
 instances be accepted together

 > Let me note that the commit in comment:5 added this note
 > {{{
 > ... Currenty [checking] if the two types are *contradicatory*,
 >  using (isNothing . tcUnifyTys).  But all the papers say
 > we should check if the two types are *equal* thus ...
 > }}}

 Thank you. So that confirms my suspicion in comment:11, bullet 3.

 > {{{
 > For now I'm leaving the bogus form because that's the way it has
 > been for years.
 > }}}

 Yes I think that's wise, given how many fragile programs are out there
 using FunDeps and overlaps.

 > Would someone like to fix the bogus-ness as suggested, and check what,
 if anything, goes wrong.

 I'm keen to help, but lack the resources or expertise.

 > It'd be worth checking what Hackage libraries build before, but fail to
 build after.

 I would guess that any library using type-level programming switches on
 `UndecidableInstances` by default, whether or not it actually needs it.

  > (...  Maybe they SHOULD fail.)    This has been wrong for a long time.

 Given the howls every time GHC tries to apply the FunDep rules more
 strictly; and given how long a time it's been wrong; I wonder if there's a
 softly-softly strategy?

 * Move from module-wide `UndecidableInstances` to a per-instance {-#
 UNDECIDABLE #-} pragma. (Same idea as with {-# OVERLAP* #-}.)
 * The '''Coverage Condition''' is defined in terms of checks on each
 instance alone, so it's just more closely targetting the logic.
 * Being in the instance gives a more in-your-face signal that this
 instance is suspicious -- essentially the programmer is acknowledging GHC
 can't necessarily enforce the '''Consistency Condition'''.
 * And I suspect a large proportion of instances do obey the '''Coverage
 Conditions'''.

 Could we go further to a per-parameter-per-instance flag?
 * The idiom I see is there's a bare type var in the instance decl, for the
 target of the FunDep. It doesn't appear elsewhere in the head, so it's
 breaking the '''Coverage Condition'''. But there's an equality constraint
 on it, where the improved type __would__ meet the '''Coverge Condition'''.
 Like:
 {{{
 instance (b ~ False) => TTypeEq a a' b    -- breaks Coverage, compare:
 instance                TTypeEq a a' False  -- Coverage OK
 }}}

 * The reason for the bare type var is to ensure this instance is {-#
 OVERLAPPABLE #-}; and a more specific instance will override it.

 With `{-# LANGUAGE  IrrefutableInstanceParams #-}` (or some equally ugly
 name), you can go:
 {{{
 instance TTypeEq a a' ~False   -- tilde prefix ? maybe too subtle
 }}}
 This:
 1. Is syntactic sugar for the form with Equality constraint, for a fresh-
 generated type var.
 2. Means the compiler can validate the '''Coverage Condition''', so this
 doesn't need {-# UNDECIDABLE #-}
 3. Lets the dog see the rabbit: the compiler can check the '''Consistency
 Condition'''.

 [To bikeshed about syntax, it's pleasing `~` is already the prefix for
 irrefutable pattern matches, and the operator for type Equality
 constraints. It appearing within the instance head is currently illegal
 syntax; but I guess with a very badly formed head, it might be confused
 with a type operator(?)]

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10675#comment:17>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler