[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