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

[GHC]

#14231: Core lint error "in result of Static argument"
-------------------------------------+-------------------------------------
        Reporter:  mpickering        |                Owner:  (none)
            Type:  bug               |               Status:  new
        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):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by osa1):

 This module has a few problems:

 - The nofib results in the module documentation are not valid anymore. I
 just
   run nofib with GHC 8.4.2 and this pass made 0 difference in allocations.

 - The running example used in documentation doesn't really work anymore.
 For
   some reason this pass doesn't transform the `map` function.

 - The pass reuses ids in binder position (i.e. binds same ids with same
 uniques
   etc. multiple times), without cloning them (probably to avoid renaming).
 I
   think this may break invariants in other places in the compiler although
 I'm
   not sure.

 Now, for this specific ticket, here's the function before SAT:

 {{{
 bindWith :: forall a. (a -> a) -> a -> a
 bindWith
   = \ (@ a_a17W) (k_atr :: a_a17W -> a_a17W) (f_ats :: a_a17W) ->
       k_atr (bindWith @ a_a17W k_atr f_ats)
 }}}

 After SAT:

 {{{
 bindWith :: forall a. (a -> a) -> a -> a
 bindWith
   = \ (@ a_a17W) (k_atr :: a_a17W -> a_a17W) (f_ats :: a_a17W) ->
       letrec {
         sat_worker_s198 :: a_a17W
         [LclId]
         sat_worker_s198
           = let {
               bindWith_r1 :: forall a. (a_a17W -> a_a17W) -> a_a17W ->
 a_a17W
               [LclId]
               bindWith_r1
                 = \ (@ a_s195) (k_s196 :: a_a17W -> a_a17W) (f_s197 ::
 a_a17W) ->
                     sat_worker_s198 } in
             k_atr (bindWith @ a_a17W k_atr f_ats); } in
       sat_worker_s198,
 }}}

 (The printer doesn't make it clear but `bindWith_r1` and `bindWith` have
 the
 same unique)

 The problem is if you ignore uniques all those `a` type variables are the
 same,
 but from the type checker's perspective they're not, which can be seen in
 the
 linter error. With `-dsuppress-uniques`:

 {{{
 Mismatch in type between binder and occurrence
 Var: bindWith
 Binder type: forall a. (a -> a) -> a -> a
 Occurrence type: forall a. (a -> a) -> a -> a
   Before subst: forall a. (a -> a) -> a -> a
 }}}

 With uniques:

 {{{
 Mismatch in type between binder and occurrence
 Var: bindWith_r1
 Binder type: forall a. (a_a17W -> a_a17W) -> a_a17W -> a_a17W
 Occurrence type: forall a. (a -> a) -> a -> a
   Before subst: forall a. (a -> a) -> a -> a
 }}}

 SAT never actually builds types, it builds terms and then calls
 `exprType`. The
 incorrect type `forall a. (a_a17W -> a_a17W) -> a_a17W -> a_a17W` is given
 to
 this term by `exprType`:

 {{{
 \ (@ a_s195) (k_s196 :: a_a17W -> a_a17W) (f_s197 :: a_a17W) ->
     sat_worker_s198
 }}}

 Arguments of this lambda is generated by this (probably broken) clone
 function:

 {{{
 clone (bndr, NotStatic) = return bndr
 clone (bndr, _        ) = do { uniq <- newUnique
                              ; return (setVarUnique bndr uniq) }
 }}}

 Where the second element of the pair is defined like this:

 {{{
 data App = VarApp Id | TypeApp Type | CoApp Coercion
 data Staticness = Static App | NotStatic
 }}}

 So this clones types, coercion, and term binders just by generating a new
 unique for them. I'm not sure if this is right way to clone binders. Then,
 as I
 said above, it reuses some ids in binder position without cloning them. I
 suspect one or both of them are causing this bug.

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