#14426: Inferred type not principle/most general? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The type inferred for `(#)` is `H a a -> H a a -> H a a` (from [https://arxiv.org/pdf/1309.5135.pdf Coroutining Folds with Hyperfunctions]) {{{#!hs 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 {{{#!hs ( # ) :: 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14426 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler