Opened 7 years ago

Last modified 9 months ago

#7026 new bug

Impredicative implicit parameters

Reported by: Ashley Yakeley Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.4.2
Keywords: ImpredicativeTypes Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

There doesn't seem to be a way to make impredicative implicit parameters work in 7.4.2:

{-# LANGUAGE ImplicitParams, ImpredicativeTypes #-}
module Bug where

    f1 :: Maybe ((?a :: Bool) => Char)
    f1 = Just 'C'

    f2 :: Maybe ((?a :: Bool) => Bool)
    f2 = Just ?a
$ ghc -c Bug.hs 

Bug.hs:5:15:
    Couldn't match expected type `(?a::Bool) => Char'
                with actual type `Char'
    In the first argument of `Just', namely 'C'
    In the expression: Just 'C'
    In an equation for `f1': f1 = Just 'C'

Bug.hs:8:15:
    Unbound implicit parameter (?a::(?a::Bool) => Bool)
      arising from a use of implicit parameter `?a'
    In the first argument of `Just', namely `?a'
    In the expression: Just ?a
    In an equation for `f2': f2 = Just ?a

I believe this used to work?

Change History (4)

comment:1 Changed 7 years ago by simonpj

difficulty: Unknown
Milestone: _|_

Ashley, I'm astonished this ever worked!

GHC's implementation of impredicative polymorphism needs love and attention. I started with quite an ambitious plan, but have lowered my sights! Now the plan is to use something along the lines of Russo/Vytiniotis QML design. The current implementation is half way between that and something more ambitious. Moreover, we have not even started to think about the interaction between impredicativity and constraint solving, which is what you are trying to do.

So think your code only ever worked by accident, and I don't see how to make it work robustly and reliably. I hope it's not mission critical to you. Apologies.

(I'm intrigued by what you were trying to do in the first place, though.)

comment:2 Changed 7 years ago by Ashley Yakeley

A nicer alternative to using a reader monad transformer is to use an implicit parameter. In my Java VM project, I define this:

type VM a = (?jvmenv :: VMEnv) => IO a

So I can use this without any lifting. Ideally VM would act like a "real" type wherever, but I run into this problem with a function that returns "Maybe (VM t)".

There are a couple of possible workarounds of course, Pulling the implicit parameter outside the "Maybe" might be acceptable, or else I can use some kind of wrapper.

comment:3 Changed 7 years ago by simonpj

Yes, maybe use a wrapper like this

newtype VM a = VM ((?jvmenv :: VMEnv) => IO a)

comment:4 Changed 9 months ago by RyanGlScott

Keywords: ImpredicativeTypes added
Note: See TracTickets for help on using tickets.