#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