#16148: Better type inference for Constraint vs Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11621, #11715, | Differential Rev(s): #13742, #16139 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
You say "don't worry about levity polymorphism", but the example you give is explicitly ruled out by our lev-poly story
Ah, that's not true: see [https://www.microsoft.com/en- us/research/publication/levity-polymorphism/ Section 7.3 of the levity- polymorphism paper], where we discuss functions like {{{ absX :: forall (r :: RuntimeRep) (a :: TYPE r). NumX a => a -> a }}} where `NumX :: forall (r :: RuntimeRep). TYPE r -> Constraint` is levity- polymorphic. Here we allow `absX` to have an arrow `a -> a` with a levity-polymorphic argument; it's just ''term binders'' that can't have levity-polymorphic types. Another point is that messing with TYPE etc affects the entire compiler. A major merit of plan (A) is that it affects the type inference engine only and is then gone. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16148#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler