s id id idに型が付かない件について

s id id idに型が付かない．

ghci> let s f g h = f h $ g h
ghci> :t s id id id

<interactive>:1:5:
    Occurs check: cannot construct the infinite type: a = a -> b
    Probable cause: `id' is applied to too few arguments
    In the second argument of `s', namely `id'
    In the expression: s id id id

フンギャー

gosh> (define (s f g x) ((f x) (g x)))
s
gosh> (s values values values)
#<subr values>

Schemeなら問題なく動くのに！ムキー！
って考えてたらもっと短く，型が付かないコードを見付けた．

ghci> let w x = x x

<interactive>:1:10:
    Occurs check: cannot construct the infinite type: t = t -> t1
    Probable cause: `x' is applied to too many arguments
    In the expression: x x
    In the definition of `w': w x = x x

いや，待てよ．Haskellには魔法の関数 unsafeCoerce があるじゃないか！

ghci> import Unsafe.Coerce
ghci> let w' x = x $ unsafeCoerce x
ghci> (w' id :: a -> a) 42
42

これを使えばさっきの関数も…！

ghci> let s' f g h = f h $ unsafeCoerce $ g h
ghci> :t s'
s' :: (t -> b1 -> b) -> (t -> a) -> t -> b
ghci> (s' id id id :: a -> a) 42
42

動いた！わーい！

何かがおかしい…

ところで s' を a -> a に特化した s'' を書こうと思ったのだが

ghci> let s'' f g h = s' f g h :: a -> a
<interactive>:1:16:
    Inferred type is less polymorphic than expected
      Quantified type variable `a' is mentioned in the environment:
        f :: t -> b1 -> a -> a (bound at <interactive>:1:8)
    In the expression: s' f g h :: a -> a
    In the definition of `s''': s'' f g h = s' f g h :: a -> a

ghci> let s'' f g h = s' f g h `asTypeOf` h
ghci> :t s''
s'' :: (t -> b1 -> t) -> (t -> a) -> t -> t
ghci> s'' id id id

<interactive>:1:4:
    Occurs check: cannot construct the infinite type: t = b1 -> t
    Probable cause: `id' is applied to too many arguments
    In the first argument of `s''', namely `id'
    In the expression: s'' id id id

ghci> let s'' :: (a -> a) -> (b -> b) -> (c -> c) -> c -> c; s'' f g h = s' f g h

<interactive>:1:54:
    Occurs check: cannot construct the infinite type: c = c -> c
    When generalising the type(s) for `s'''

分からん…