[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 goldfire):

 Points well taken, but I'm a little uncomfortable with the directional of
 travel, because we ''are'' making things worse: the `reflection` library
 depends critically on `unsafeCoerce`. If we implement `with`, then we've
 essentially blessed this operation as safe. So the behavior is the same,
 but what was previously considered unsafe is now safe. It doesn't sound
 great to me.

 The example in comment:23 is, in my view, an infelicity in the design of
 the language. I'm not convinced that rejecting `cmp` is a good idea, but
 it is dangerously implementation-dependent. Indeed in GHC the choice of
 `Ord` dictionary might change between minor releases or depending on what
 order functions are written in a module.

 Here's an idea, based on visible type application (that is, `id @Int ::
 Int -> Int`) that allows us to specify usually-inferred parameters:
  * Extend the visible type application mechanism to work with dictionaries
 (that is, constraints).
  * Add the ability to bind a variable to an inferred parameter in a
 pattern, with `@`.
  * Reject code that uses dictionaries ambiguously, now that we have a
 workaround.

 The example from comment:23 is now rejected. But here is the working
 version:

 {{{
 cmp :: SomeOrd a -> SomeOrd a -> Ordering
 cmp (SomeOrd @_ @d1 a) (SomeOrd @_ @_d2 b) = compare @_ @d1 a b
 }}}

 All the `@_` arguments above are because we don't care about the type
 variables, which come before the dictionaries. Here, we've explicitly
 chosen the first dictionary, so there is no ambiguity or implementation-
 dependence.

 Unfortunately, implementing this plan is a ways off. Perhaps we could just
 special-case `with` to error on ambiguity (naturally, this wouldn't break
 existing code) and know that we'll have a better solution later.

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