[GHC] #11715: Constraint vs *

GHC ghc-devs at haskell.org
Tue Dec 6 17:48:14 UTC 2016


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

 Let's imagine a future where `(->) :: forall (r1 :: RuntimeRep) (r2 ::
 RuntimeRep). TYPE r1 -> TYPE r2 -> Type`. Then, we have the well-typed
 `(->) ConstraintRep LiftedRep (C a) (a -> a)`. But if we normalize w.r.t.
 newtypes (e.g., in `normaliseFfiType`), then we'll get `(->) ConstraintRep
 LiftedRep (a -> a) (a -> a)`, which is ill-kinded. In this case, we can
 just change `ConstraintRep` to `LiftedRep` as we normalize, but it's not
 clear that it will always be so easy.

 (But maybe it really will be, because we tend not to unwrap newtypes under
 other type constructors.)

 There's also the niggling problem that the type safety proofs in the
 presence of newtype axioms explicitly assume that axioms are homogeneous.
 But maybe this is unnecessary.

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


More information about the ghc-tickets mailing list