[Haskell-cafe] Strange context reduction with partial application and casting

[Daniel Fischer]

On Saturday 02 July 2011, 20:23:48, Wonchan Lee wrote:
> Hi cafe,
> 
> I found some strange phenomenon when I was hanging around with GHCi.
> Please see the following interaction:
> 
> GHCi, version 7.0.3: http://www.haskell.org/ghc/  :? for help
> Loading package ghc-prim ... linking ... done.
> Loading package integer-gmp ... linking ... done.
> Loading package base ... linking ... done.
> Loading package ffi-1.0 ... linking ... done.
> Prelude> let f a b c d = a == b && c == d
> Prelude> :t f
> f :: (Eq a, Eq a1) => a -> a -> a1 -> a1 -> Bool
> Prelude> let g = f 1
> Prelude> :t g
> g :: Integer -> () -> () -> Bool
> 
> Here I expect that the type of g is (Eq a) => Integer -> a -> a -> Bool.
> But suddenly all the context in the type is gone and I have some
> strange thing with unit type in it.
> I tried another example to get what I expected at the first time:
> 
> Prelude> let g = f :: (Eq a) => Int -> Int -> a -> a -> Bool
> Prelude> :t g
> g :: Int -> Int -> () -> () -> Bool
> 
> The resulting type was different from one that I want to cast into.
> I know that Haskell tries to reduce the context in the type when
> there's sufficient information to do it.
> However, this goes too far from what I think normal.
> 
> Is this intended behavior or just a bug?

It's intended, caused by the monomorphism restriction.
You bind g by a binding with neither type signature nor function arguments, 
therefore the monomorphism restriction (cf. language report, section 4.5) 
says g must have a monomorphic type. Per the report, "let g = f 1" should 
not compile at all, because one of the requirements for type defaulting is 
that a numeric class constraint be present, but the second type only has an 
Eq constraint; however, ghci uses extended default rules (too many 
ambiguous type errors would arise otherwise) and thus defaults that type 
variable to ().

You can get the expected behaivour by

- giving g a type signature (in your last example, the type signature was 
for f)
let g :: Eq a => Int -> Int -> a -> a -> Bool; g = f

- binding g with a function binding, i.e. with arguments
let g a b c d = f a b c d
(let g a = f a is already enough, all that is required to get a polymorphic 
type for g is one function argument in the binding)

- disabling the monomorphism restriction
:set -XNoMonomorphismRestriction
let g = f