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

17 Mar 2016

      #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):

 Indeed; see this (in `Kind.hs`)
 {{{
 Note [Kind Constraint and kind *]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The kind Constraint is the kind of classes and other type constraints.
 The special thing about types of kind Constraint is that
  * They are displayed with double arrow:
      f :: Ord a => a -> a
  * They are implicitly instantiated at call sites; so the type inference
    engine inserts an extra argument of type (Ord a) at every call site
    to f.

 However, once type inference is over, there is *no* distinction between
 Constraint and *.  Indeed we can have coercions between the two. Consider
    class C a where
      op :: a -> a
 For this single-method class we may generate a newtype, which in turn
 generates an axiom witnessing
     C a ~ (a -> a)
 so on the left we have Constraint, and on the right we have *.
 See Trac #7451.

 Bottom line: although '*' and 'Constraint' are distinct TyCons, with
 distinct uniques, they are treated as equal at all times except
 during type inference.
 }}}
 This is a true wart, which I have always longed to expunge.

 And actually, now we heterogeneous equalities, maybe we can!!  Perhaps we
 could have
 {{{
 newtype C a :: Constraint = MkC (a->a)   -- Not legal source code
 }}}
 leading to an axiom
 {{{
 axC :: forall (a:*). (C a :: Constraint) ~R (a->a :: *)
 }}}
 That is, `*` and `Constraint` both classify values, but different kinds of
 values.  Is that ok?

 Or, I suppose we could say
 {{{
 type Constraint = TYPE ConstraintRep
 }}}
 That would be even better, because  we can certainly have `Ord a -> a` (at
 least in Core), and even `((->) (Ord a))`.

 Does that seem plausible?  I like it.

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