Re: [GHC] #14231: Core lint error "in result of Static argument"

10 Jul 2018

      #14231: Core lint error "in result of Static argument"
-------------------------------------+-------------------------------------
        Reporter:  mpickering        |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.5
      Resolution:                    |             Keywords:
                                     |  StaticArgumentTransformation
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D4945
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Aargh.  I'm an idiot.  My claim that cloning is unnecessary is
 utterly wrong.  Here's a fixed version of the latter part of comment:13.

 We want to generate this:
 {{{
    f :: forall a b. (a,b) -> b -> Int
    f = /\a b. \(x:(a,b)) (y:b).
        letrec fwrk = /\a \(x:(a,b).
                         REPLACE (f <ty> b <e> y) WITH (fwrk <ty> <e>)
                         IN  <body>
        in fwrk a x
 }}}
 Here `fwrk` is the local, recursive worker, which has free variables `b`'
 and `y::b`.
 Notice that the binders of `fwrk`, namely `a` and `x::(a,b)` must be
 identical (same
 unique) as the originals, because they are mentioned in `<body>`.

 What is this "REPLACE" business?  We want to replace a recusive call to
 `f` with
 a call to `fwrk`.  The easy way to do this is with a non-recursive let,
 later inlined:
 {{{
    f = /\a b. \(x:(a,b)) (y:b).
        letrec fwrk :: forall a. (a,b) -> Int
               fwrk = /\a \(x:(a,b).
                         let f :: forall a b1. (a,b) -> b -> Int
                             f = /\a _ \(x::(a,b) (_::b). fwrk a x
                         in <body>
        in fwrk a x
 }}}
 We must use the ''same'' unique for that inner `f`:
 we are deliberately shadowing its outer binding.

 Notice too that I used underscores (i.e. freshly-cloned variables that are
 never
 referred to) for the static variables.  Reason: `fwrk t` expects an
 argument of type
 `(t,b)`, where `b` scopes globally over the entire definition of `fwrk`.
 We ''cannot''
 write
 {{{
                         let f :: forall a b. (a,b) -> b -> Int
                             f = /\a b \(x::(a,b) (y::b). fwrk a x
 }}}
 becuase then the call to `fwrk` is ill-typed.
 This is what `Note [Binder type capture]` is about.  We should clone the
 static binders; and it does no harm to clone everything I suppose.

 ------------------
 So what is wrong in commnet:8.  Here's the actual error message
 {{{
     In the expression: bindWith @ a_a17R k_atm f_atn
     Mismatch in type between binder and occurrence
     Var: bindWith_rqJ
     Binder type: forall a. (a_a17R -> a_a17R) -> a_a17R -> a_a17R
     Occurrence type: forall a. (a -> a) -> a -> a
       Before subst: forall a. (a -> a) -> a -> a
 }}}
 Ah!  Indeed in our running example, the REPLACE binding for `f` has type
 {{{
                         let f :: forall a b1. (a,b) -> b -> Int
                             f = /\a _ \(x::(a,b) (_::b). fwrk a x
 }}}
 and indeed that is not the type of the top-level `f`. But each
 ''occurrence'' of `f` has the top of the top-level `f` and Lint is
 objecting that there seems to be an inconsistency.  If we just let
 it inline, everything would be fine.

 How tiresome.   Using a let-binding to do the REPLACE stuff is not as
 convenient as it seems :-(.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:15
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler