
#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #1241, #2247, | Differential Rev(s): Phab:D69 #8356, #9103, #9227 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:63 goldfire]: Hi Richard, I think we're already (at GHC 7.10/8.0) pretty close to being able to write your `class Terrible`.
{{{ class Terrible a b | a -> b instance Terrible Int Bool instance Terrible Int Char }}}
See Iavor's example comment:12:ticket:10675. Or this https://mail.haskell.org/pipermail/glasgow-haskell- users/2017-April/026507.html . Both examples rely on `UndecidableInstances` and overlaps. Not necessrily `OverlappingInstances`: in Iavor's example, the FunDeps are non-full.
{{{ foo :: Terrible a b => a -> b foo = undefined }}}
and we call `show (foo (5 :: Int))`. GHC has to figure out what type the
argument to `show` has so it can supply the right `Show` instance. In this case, the type inferred for `foo (5 :: Int)` will either be `Bool` or `Char`, depending on the whims of GHC at the moment. In those examples I cited, GHC does make a predictable choice (so not entirely on a whim). But it's inconsistent between the FunDeps, so very sensitive to subtle changes in (apparently) unrelated parts of the program/some distant module. For example, merely adding a type signature could trigger selecting a different instance.
... Much like with `IncoherentInstances`, it's up to the user not to shoot themselves in the foot.
With a great deal of hindsight, what `Undecidable` means in these cases is: * The type specified in the instance head isn't mechanically derivable from the other type parameters. So the programmer is saying "trust me, at any use site, you'll be able to figure out the right type". * GHC can't follow the trail of instance constraints/instantiation -- especially because it might need looking at other modules and/or a very long chain. * So `Undecidable` means GHC can't/won't decide whether any given FunDep is instantiated consistently across all the instances. I'm not sure that's abundantly well explained in the docos. OTOH, there's some type-level programming that deliberately exploits that inconsistency -- such as anything that despatches on a type-level type-equality condition (the whole of the HList library, as originally developed). Closed type families is nowadays a much more hygienic mechanism. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:70 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler