[GHC] #15710: Should GHC accept a type signature that needs coercion quantification?

[GHC]

#15710: Should GHC accept a type signature that needs coercion quantification?
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.1
      Resolution:                    |             Keywords:  TypeInType
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 #14648 you argued that `(t1 ~# t2)` should not be a constraint, should
 not return True to `isPredTy`, and should not be an invisible parameter,
 implicitly instantiated at call sites.

 Here you seem to be arguing the exact opposite!

 I'm uncomfortable with forcing the the user to deal with both `(~)` and
 `(~#)`; I wanted the latter to be an implementation detail.  Even putting
 it in a constraint tuple like `f :: (Num a, a ~ b) => blah` is problematic
 if `a~b` is unlifted/unboxed.

 Our "all constraints are boxed" story was working perfectly well right up
 to this, when we add coercion quantification.  But I don't see a way to
 reconcile it with coercion quantification.  Alas.

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