Inferred type not principle/most general?
The type inferred for (#)
is H a a -> H a a -> H a a
(from Coroutining Folds with Hyperfunctions)
newtype H a b = Fn { invoke :: H b a -> b }
-- ( # ) :: H a a -> H a a -> H a a
f # g = Fn (\k -> invoke f (g # k))
but a more general type is actually
( # ) :: H b c -> H a b -> H a c
f # g = Fn (\k -> invoke f (g # k))
Is this expected or a blind spot in type inference
Same thing in ghci
$ ghci -ignore-dot-ghci
GHCi, version 8.3.20170920: http://www.haskell.org/ghc/ :? for help
Prelude> :set prompt "> "
>
> newtype H a b = Fn { invoke :: H b a -> b }
>
> f # g = Fn (\k -> invoke f (g # k))
> :t ( # )
( # ) :: H a a -> H a a -> H a a
>
> let ( # ) :: H b c -> H a b -> H a c; f # g = Fn (\k -> invoke f (g # k))
> :t ( # )
( # ) :: H b c -> H a b -> H a c
Interestingly writing it in terms of fix
does not type check with the more general type
> import Data.Function
> :t fix $ \self -> \f g -> Fn (\k -> invoke f (self g k))
fix $ \self -> \f g -> Fn (\k -> invoke f (self g k))
:: H a a -> H a a -> H a a
> :t (fix $ \self -> \f g -> Fn (\k -> invoke f (self g k))) :: H b c -> H a b -> H a c
<interactive>:1:2: error:
• Couldn't match type ‘b1’ with ‘a1’
‘b1’ is a rigid type variable bound by
an expression type signature:
forall b1 c1 a1. H b1 c1 -> H a1 b1 -> H a1 c1
at <interactive>:1:60-82
‘a1’ is a rigid type variable bound by
an expression type signature:
forall b1 c1 a1. H b1 c1 -> H a1 b1 -> H a1 c1
at <interactive>:1:60-82
Expected type: H b1 c1 -> H a1 b1 -> H a1 c1
Actual type: H a1 a1 -> H a1 a1 -> H a1 a1
• In the expression:
(fix $ \ self -> \ f g -> Fn (\ k -> ...)) ::
H b c -> H a b -> H a c
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |