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

 I have a couple of reservations about this ticket.

 Issue 1)

 {{{#!hs
 reify :: c => c
 with  :: c -> (c => r) -> r
 }}}

 are morally close to `reflect` and `reify` from the `reflection` package
 respectively. (Chung-chieh Shan has a pretty compelling argument for why
 your `reify` is actually a `reflect`.)

 With the stated intent of working around the `Dict` hack, they work fine!

 However, they can also be used to model reflection in a dangerous way: By
 letting you pack up an arbitrary Int => ... now the instance for "Int"
 isn't unique. This means that the category of constraints isn't thin, and
 that now we care about provenance about where you got the Int from. This
 yields all the same problems as

 {{{#!hs
 class (?foo :: Int) => Bar a
 }}}

 from

 {{{#!hs
 class Int => Bar a
 }}}

 whereas we very explicitly disallow the former today. Right now every way
 you can compose an entailment in Constraint in the absence of
 IncoherentInstances and ImplicitParams is unique. This lets things like
 `Set` know the instance won't change on it between `insert` and `lookup`.
 I'm very scared of letting in something that would break that guarantee.

 Going the other way, and letting you bring constraints out to the right
 side of the => isn't hazardous, as with and reify don't give you tools to
 construct such a dictionary, and this just lets you move things around in
 the same manner as `Dict` does today. But with `Constraint = *`, it isn't
 clear how to keep that safe.

 `Given` in the `reflection` library, which provides this functionality
 today is actually being demoted to a supplemental package due to the
 amount of pain and confusion it causes users when multiple instances find
 themselves in scope.

 `reify` and `reflect` do not have those problems due to the quantifier.

 To preserve your desire to embed Constraint into * without overhead, in
 theory `Dict` could just be a magical newtype, put on and removed by the
 equivalent of your `reify` and `with` combinators:

 {{{
 dict :: c => Dict c
 with :: Dict c -> (c => r) -> r
 }}}

 This avoids the `class Int => Bar a` issue entirely and doesn't interfere
 with a sound reflection story.

 Issue 2)

 It is a fairly common newbie error to write `foo :: Ord a -> a -> Set a`
 -- which would now very confusingly pass the type system rather than get
 caught. We should at least have the discussion about if this is desirable.

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