Opened 5 years ago

Closed 5 years ago

Last modified 5 years ago

#7594 closed bug (worksforme)

GHCi becomes confused about IO type

Reported by: Khudyakov Owned by:
Priority: normal Milestone:
Component: GHCi Version: 7.6.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: polykinds/T7594
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs           #-}
{-# LANGUAGE Rank2Types      #-}
import GHC.Prim (Constraint)

class    (c1 t, c2 t) => (:&:) (c1 :: * -> Constraint) (c2 :: * -> Constraint) (t :: *)
instance (c1 t, c2 t) => (:&:) c1 c2 t

data ColD c where
  ColD :: (c a) => a -> ColD c

app :: (forall a. (c a) => a -> b) -> ColD c -> b
app f (ColD x) = f x

q :: ColD (Show :&: Real)
q = ColD (1.2 :: Double)

In the interactive mode it's possible to confuse GHCi about IO type. It tries to show expression instread of executing it.

*Main> app print q

    No instance for (Show (IO ())) arising from a use of `print'
    Possible fix: add an instance declaration for (Show (IO ()))
    In a stmt of an interactive GHCi command: print it

Change History (2)

comment:1 Changed 5 years ago by simonpj

difficulty: Unknown
Resolution: worksforme
Status: newclosed

Hmm. Absolutely right, and this happens for 7.6.2 too. However with HEAD we get:

    Couldn't match type `b' with `IO ()'
      `b' is untouchable
        inside the constraints ((:&:) Show Real a)
        bound by a type expected by the context:
                   (:&:) Show Real a => a -> b
        at <interactive>:2:1-11
      `b' is a rigid type variable bound by
          the inferred type of it :: b at <interactive>:2:1

This is actually right, although the error message is not so easy. We know that

print :: Show a => a -> IO ()

We also know (by way of the argument q, that c = (Show :&: Real) a. So, to check that print is a valid argument to app, we must check that

From          (Show :&: Real) a
prove that    (Show a, beta ~ IO ())

where beta is a unification variable (as-yet-unknown type) obtained by instantiating app.

Well, you say, we can choose beta to be IO () and we are done. But not so: in general the "From" constraints might include GADT-style equalites, and GHC is careful NOT to unify under equality constraints. (See the Modular type inference with local assumptions paper.) That's why beta is "untouchable".

Easily fixed by saying app print q :: IO (), and that works fine.

I am strongly dis-inclined to attempt to find out what's happening in 7.6! So I propose just to close this. I might add a regression test though.


comment:2 Changed 5 years ago by simonpj

Test Case: polykinds/T7594
Note: See TracTickets for help on using tickets.