[GHC] #11715: Constraint vs *

[GHC]

#11715: Constraint vs *
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.0.1-rc1
  checker)                           |
      Resolution:                    |             Keywords:  Typeable
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 int-index):

 I don't think that `cmp` should be rejected. I see no problem that GHC
 just picks one of the available dictionaries. Let me explain why.

 Currently, all of those types are equivalent:

 * `(a, b) => t`
 * `(b, a) => t`
 * `a => b => t`
 * `b => a => t`

 Also, those types are equivalent:

 * `c => t`
 * `(c, c) => t`
 * `c => c => t`

 This means that the only thing that identifies a value to the left of `=>`
 is its type. Whereas you can pass two distinct `Int`s to a function
 explicitly (`Int -> Int -> r`), you can't do the same implicitly (`Given
 Int => Given Int => r` ~ `Given Int => r`). It is therefore reasonable to
 expect that there's only *one unique value* of each type to the left of
 `=>`. If there are more, you can't distinguish between them anyway. This
 plays really well with type classes: since instances are coherent, `Ord a`
 is a unique value for each `a`.

 With the `Given`/`given`/`give` machinery from `reflection` we can now
 enrich the context with different values of the same type. I say that this
 is a violation of the philosophy behind `=>` and we don't want features
 (such as explicitly binding dictionaries using `@`-syntax) that get us
 further down this road.

 Partial solutions will not help. Say we forbid using nested `give`s with
 the same type as proposed in comment:22: the example in comment:24
 demonstrates that we can violate the "one type - one value" principle
 without using nested `give`s by packaging the dictionaries in a GADT.

 I propose the following: let's get rid of `Given` and allow arbitrary
 things of kind `Type` to the left of `=>`. However, let's not call `give`
 some pretty name like `with` and add special casing; instead, let's call
 it `incoherentWithDict` and put it into a deep dark corner of `GHC.Exts`.

 Why bother at all? Now we can implement the safe interface
 (`Reifies`/`reflect`/`reify` from `reflection`) without `unsafeCoerce`,
 using `incoherentWithDict` instead.

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