#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature | Status: new request | Milestone: 7.10.1 Priority: high | Version: 7.7 Component: Compiler | Keywords: Resolution: | Operating System: Unknown/Multiple Differential Revisions: Phab:D69 | Type of failure: None/Unknown Architecture: | Test Case: Unknown/Multiple | Blocking: Difficulty: Unknown | Blocked By: | Related Tickets: #1241, | #2247, #8356, #9103, #9227 | -------------------------------------+------------------------------------- Comment (by simonpj): I think we are all agreed that type inference must be sound. But, as mentioned above, "sound" for GHC means that * If the program passes the type checker, the elaborated Core program satisfies Core Lint. * If a program satisfies Core Lint, it enjoys preservation and progress (of the Core program); it cannot seg-fault. In operational terms I think the change proposed is well specified: look at comment:14, especially the user manual section and the three bullets at the end of the comment. The question at issue is not soundness, but rather * Precisely which programs satisfy the type inference engine? * Is type inference complete? I.e. does it find a type for every program specified by the first bullet? * Is type inference robust? I.e. can a small change in the program (e.g. swapping the order of arguments to a function) make the difference between type inference succeeding and failing? * Is the elaborated program coherent? I.e. is it well specified what the result of running that program will be? The effect of `-XDysFunctionalDependencies` on these aspects of type inference is not well understood. But it seems a much more benign form of allowing the programmer saying "trust me please" than `unsafeCoerce`, for example, because the soundness guarantee is not threatened. The `-XUndecideableInstances` flag is somewhat similar, in that it continues to guarantee soundness, but allows type inference to diverge. This could perfectly well be a per-instance pragma, rather than a module- wide language extensions. Something like {{{ instance {-# DYSFUNCTIONAL#-} Monad m => CTest X (m Int) where ... }}} That might be better, actually; it's more precisely targeted. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler