[GHC] #14426: Inferred type not principle/most general?

6 Nov 2017


      #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