Re: [GHC] #9334: Implement "instance chains"

25 Aug 2016

      #9334: Implement "instance chains"
-------------------------------------+-------------------------------------
        Reporter:  diatchki          |                Owner:  diatchki
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.9
  checker)                           |
      Resolution:                    |             Keywords:
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 garrett):

 Replying to [comment:14 Iceland_jack]:
...
Another
 [https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70#pdf-
 type-classes-and-instance-chains-a-relational-approach-1 approach] that
 uses the module system to hide this class and type:
{{{#!hs
class Fail t
data TypeExists t
}}}
and uses it as
{{{#!hs
instance Fail (TypeExists t) => HasNone t (Cons t ts)
}}}
This isn't really the goal of `fails` instances (or other negative
 information) in instance chains.  Negative information is used to direct
 instance selection; encodings, like this one, are only useful for the same
 purpose if the compiler knows that the `Fail (TypeExists t)` predicate is
 unsatisfiable.

 For an example that doesn't rely on `fails`, consider the following

 {{{#!hs
 class F t u | t -> u
 instance F Bool Int

 class C t
   where f :: t -> t -> t
 instance F t Bool => C t
   where f x y = x
 else C t
   where f x y = y
 }}}

 We expect that `f True False` evaluates to `False`; but, to know that the
 first clause of the chain does not apply, we need to know that the
 constraint `F Bool Bool` cannot hold (not just that it does not hold at
 the current point).  In this case, we know that because of the functional
 dependency on `F`.

 This is not to say that a sufficient smart solver might not be able to
 determine that the `Fail (...)` or `Any` constraints are unsatisfiable.
 Just that a design which attempts to use these constraints in the role of
 the `fails` constraints in instance chains must presuppose such a solver.

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