The impossible happened with implicit parameters

[Ashley Yakeley]

{-# OPTIONS -XImplicitParams -XRankNTypes #-}
module Bug where

t :: forall a. ((?p :: Int) => a) -> String
t _ = "Hello"

f :: (forall a. a -> String) -> Int
f _ = 3

result :: Int
result = f t

$ ghc -c Bug.hs
ghc: panic! (the 'impossible' happened)
  (GHC version 6.10.1 for x86_64-unknown-linux):
	TcTyFuns.flattenType: unexpected PredType

[Ashley Yakeley]

Note that with this, it compiles fine:

result :: Int
result = f (\a -> t a)

[simonpj]

Manuel, could you look into this, pls?

Simon

[igloo]

In 6.12 and HEAD, we now get a nice error:

u.hs:11:9:
    Occurs check: cannot construct the infinite type:
      a = (?p::Int) => a
    In the first argument of `f', namely `t'
    In the expression: f t
    In the definition of `result': result = f t

[Ashley Yakeley]

Better than panic, but it's still wrong, because "a = (?p::Int) => a" is not an infinite type.

For instance, a = "(?p::Int) => String" satisfies "a = (?p::Int) => a".

[simonpj]

You're right. There was another bug lurking.

Mon Nov 30 09:44:41 PST 2009  simonpj@microsoft.com
  * Fix Trac #3102: pre-matching polytypes
  
  When *pre-matching* two types
       forall a. C1 => t1  ~  forall a. C2 => t2
  we were matching t1~t2, but totally ignoring C1,C2
  That's utterly wrong when pre-matching
         (?p::Int) => String  ~  a
  because we emerge with a:=String!
  
  All this is part of the impredicative story, which is about
  to go away, but still.
  
  Worth merging this to 6.12

    M ./compiler/typecheck/TcUnify.lhs -2 +3

Merge if possible to 6.12.

Thanks for being persistent.

Simon

[igloo]

Merged