[GHC] #11715: There's something fishy going on with Constraint

[GHC]

#11715: There's something fishy going on with Constraint
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  8.0.1-rc1
  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 simonpj):

 In a phone conversation yesterday we also developed an alternative plan to
 comment:5, namely '''make `Constraint` and `*` the same in Haskell'''.
 Thus:

 * `type Constraint = *`.  So the two are the same even in source Haskell.

 * A type sig like `f :: Int => Int` becomes kind-correct.  But we can
 still rejects it in `checkValidType`, in the same way that we reject
 higher-rank types when that extension is not enabled.

   Ditto `f :: Ord a -> Int`

 '''Disadvantages'''

 This signature for `f` is currently rejected as ill-kinded:
 {{{
 type family F a :: Constraint
 type instance F Int = Ord Bool
 ...

 f :: F a -> a  -- Currently ill-kinded
 }}}
 but would now be accepted, because `checkValidType` could not easily
 reject it.  More seriously
 {{{
 g :: F a => a -> a
 }}}
 would also be accepted even if `F` plainly returned types not constraints.

 '''Advantages'''

 * The proposal would eliminate the need for constraint tuples distinct
 from ordinary value tuples, which would be good.

 * If we were to silence `checkValidType` (with a language extension), it
 would also allow functions like
 {{{
 reify :: c => c
 with  :: c -> (c => r) -> r
 }}}
   which allow you to get a dictionary as a value, and use it elsewhere.
 Currently this requires the "Dict trick":
 {{{
 data Dict c where
   Dict :: c => Dict c

 reifyD :: c => Dict c
 reifyD = Ditc

 withD :: Dict c -> (c => r) -> r
 withD Dict k = k
 }}}
   but the Dict trick actually does boxing and unboxing because it involves
 a `data` type.  It would be more direct not to require this.

 * Another example: perhaps `TypeRep a` (the type) and `Typeable a` (the
 constraint) could be the same thing.  Thus
 {{{
 f :: TypeRep a => TypeRep b -> blah
 }}}
   would mean that the first arg was passed implicitly and the second
 implicitly.

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