[GHC] #14231: Core lint error "in result of Static argument"
#14231: Core lint error "in result of Static argument" -------------------------------------+------------------------------------- Reporter: mpickering | 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: -------------------------------------+------------------------------------- Whilst investigating #14211 I encountered a core lint error. {{{ {-# LANGUAGE CPP #-} {-# LANGUAGE RankNTypes #-} module Async where data AsyncT m a = AsyncT { runAsyncT :: forall r. Maybe Int -- state -> m r -- stop -> (a -> Maybe Int -> Maybe (AsyncT m a) -> m r) -- yield -> m r } ------------------------------------------------------------------------------ -- Monad ------------------------------------------------------------------------------ {-# INLINE bindWith #-} bindWith :: (forall c. AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b bindWith k (AsyncT m) f = AsyncT $ \_ stp yld -> m Nothing stp (\a _ m -> (\x -> (runAsyncT x) Nothing stp yld) $ maybe (f a) (\r -> f a `k` (bindWith k r f)) m ) }}} Compile with `ghc -O2 -fno-worker-wrapper -fstatic-argument-transformation -dcore-lint`. Error: {{{ *** Core Lint errors : in result of Static argument *** <no location info>: warning: In the expression: bindWith @ m_aV5 @ a_aV6 @ b_aV7 k_aSU x_aX3 f_aSW Mismatch in type between binder and occurrence Var: bindWith_rpi Binder type: forall (m1 :: * -> *) a1 b1 . (forall c . AsyncT m_aV5 c -> AsyncT m_aV5 c -> AsyncT m_aV5 c) -> AsyncT m_aV5 a_aV6 -> (a_aV6 -> AsyncT m_aV5 b_aV7) -> AsyncT m_aV5 b_aV7 Occurrence type: forall (m :: * -> *) a b . (forall c . AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b Before subst: forall (m :: * -> *) a b . (forall c . AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b *** Offending Program *** }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14231: Core lint error "in result of Static argument" -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => StaticArgumentTransformation Comment: That indeed looks like a (not very serious) bug. But Matthew, I think you are studying SAT anyway. Maybe this one will come out in the wash as you do so? If so it may not be worth fixing the current pass? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14231: Core lint error "in result of Static argument" -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 mpickering): I think this is happening because of `Note [Shadow binder]` which sounds quite dubious. {{{ Note [Shadow binding] ~~~~~~~~~~~~~~~~~~~~~ The calls to the inner map inside body[map] should get inlined by the local re-binding of 'map'. We call this the "shadow binding". But we can't use the original binder 'map' unchanged, because it might be exported, in which case the shadow binding won't be discarded as dead code after it is inlined. So we use a hack: we make a new SysLocal binder with the *same* unique as binder. (Another alternative would be to reset the export flag.) }}} Then the shadowed binder is constructed from the unique of the old binder and the type of the shadowed_rhs. {{{ shadow_bndr = mkSysLocal (occNameFS (getOccName binder)) (idUnique binder) (exprType shadow_rhs) }}} It seems that the idea here is that we want to replace the self-recursive call with a call to the sat_worker. The mechanism for this is to create a local binding which shadows the top-level id which will be inlined in a later pass. In other parts of the compiler the way this would be achieved is to create a new top-level definition for the satted version of the function and then a `RULE` which rewrites the old version to the new version. Would that be preferable here as well? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14231: Core lint error "in result of Static argument" -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 simonpj):
Would that be preferable here as well?
I'm not sure. If it's still relevant, could you give a standalone example to show what you mean? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14231: Core lint error "in result of Static argument" -------------------------------------+------------------------------------- Reporter: mpickering | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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 monoidal): Simplification of the bug report: {{{ module Async where bindWith :: (a -> a) -> a -> a bindWith k f = k (bindWith k f) }}} and as previously `ghc -O2 -fno-worker-wrapper -fstatic-argument- transformation -dcore-lint`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by osa1): * version: 8.2.1 => 8.5 Comment: Confirmed on GHC HEAD. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Description changed by osa1: Old description:
Whilst investigating #14211 I encountered a core lint error.
{{{ {-# LANGUAGE CPP #-} {-# LANGUAGE RankNTypes #-}
module Async where
data AsyncT m a = AsyncT { runAsyncT :: forall r. Maybe Int -- state -> m r -- stop -> (a -> Maybe Int -> Maybe (AsyncT m a) -> m r) -- yield -> m r }
------------------------------------------------------------------------------ -- Monad ------------------------------------------------------------------------------
{-# INLINE bindWith #-} bindWith :: (forall c. AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b bindWith k (AsyncT m) f = AsyncT $ \_ stp yld -> m Nothing stp (\a _ m -> (\x -> (runAsyncT x) Nothing stp yld) $ maybe (f a) (\r -> f a `k` (bindWith k r f)) m ) }}}
Compile with `ghc -O2 -fno-worker-wrapper -fstatic-argument- transformation -dcore-lint`.
Error: {{{ *** Core Lint errors : in result of Static argument *** <no location info>: warning: In the expression: bindWith @ m_aV5 @ a_aV6 @ b_aV7 k_aSU x_aX3 f_aSW Mismatch in type between binder and occurrence Var: bindWith_rpi Binder type: forall (m1 :: * -> *) a1 b1 .
(forall c . AsyncT m_aV5 c -> AsyncT m_aV5 c -> AsyncT m_aV5 c) -> AsyncT m_aV5 a_aV6 -> (a_aV6 -> AsyncT m_aV5 b_aV7) -> AsyncT m_aV5 b_aV7 Occurrence type: forall (m :: * -> *) a b .
(forall c . AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b Before subst: forall (m :: * -> *) a b .
(forall c . AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b *** Offending Program *** }}}
New description: Whilst investigating #14211 I encountered a core lint error. {{{ {-# LANGUAGE CPP #-} {-# LANGUAGE RankNTypes #-} module Async where data AsyncT m a = AsyncT { runAsyncT :: forall r. Maybe Int -- state -> m r -- stop -> (a -> Maybe Int -> Maybe (AsyncT m a) -> m r) -- yield -> m r } ------------------------------------------------------------------------------ -- Monad ------------------------------------------------------------------------------ {-# INLINE bindWith #-} bindWith :: (forall c. AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b bindWith k (AsyncT m) f = AsyncT $ \_ stp yld -> m Nothing stp (\a _ m -> (\x -> (runAsyncT x) Nothing stp yld) $ maybe (f a) (\r -> f a `k` (bindWith k r f)) m ) }}} Compile with `ghc -O2 -fno-worker-wrapper -fstatic-argument-transformation -dcore-lint`. Error: {{{ *** Core Lint errors : in result of Static argument *** <no location info>: warning: In the expression: bindWith @ m_aV5 @ a_aV6 @ b_aV7 k_aSU x_aX3 f_aSW Mismatch in type between binder and occurrence Var: bindWith_rpi Binder type: forall (m1 :: * -> *) a1 b1 . (forall c . AsyncT m_aV5 c -> AsyncT m_aV5 c -> AsyncT m_aV5 c) -> AsyncT m_aV5 a_aV6 -> (a_aV6 -> AsyncT m_aV5 b_aV7) -> AsyncT m_aV5 b_aV7 Occurrence type: forall (m :: * -> *) a b . (forall c . AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b Before subst: forall (m :: * -> *) a b . (forall c . AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b *** Offending Program *** }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): Looking at this again; I realized that we don't need any flags to trigger some lint warnings in the original program (the `Async` module): {{{ $ ghc-stage2 Async.hs -dcore-lint -fforce-recomp -O0 [1 of 1] Compiling Async ( Async.hs, Async.o ) *** Core Lint warnings : in result of Simplifier *** Async.hs:25:1: warning: [RHS of bindWith :: forall (m :: * -> *) a b. (forall c. AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b] INLINE binder is (non-rule) loop breaker: bindWith *** Core Lint warnings : in result of Simplifier *** Async.hs:25:1: warning: [RHS of bindWith :: forall (m :: * -> *) a b. (forall c. AsyncT m c -> AsyncT m c -> AsyncT m c) -> AsyncT m a -> (a -> AsyncT m b) -> AsyncT m b] INLINE binder is (non-rule) loop breaker: bindWith }}} This warning disappears if I remove the `INLINE` pragma. Not sure if this is a bug (it's a warning, not an error) but maybe useful to know. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
Looking at this again; I realized that we don't need any flags to
#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 monoidal): Replying to [comment:7 osa1]: trigger some lint warnings in the original program (the `Async` module): This is a different issue; GHC won't inline a self-recursive definition (e.g. `x :: a; x = x`) even if it's marked as INLINE. We could have better messaging about this, I believe this is ticket #9418. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by osa1): * status: new => patch * differential: => Phab:D4945 Comment: In comment:8 I mentioned two problems: 1. Weird shadowing code to avoid renaming. 2. Weird binder cloning. It turns out only fixing (1) is enough to close this ticket. It's easy to fix (2) too (we just need to clone all binders of a definition with `CoreSubst.cloneIdBndrs`) but my patch doesn't include that for now. I validated GHC HEAD with `-fstatic-argument-transformation` and got a bunch of failures. I'll validate again with Phab:D4945 (and with `-fSAT`), and then validate again with my fix for (2) to see if that fixes any existing failures. (I don't have a reproducer for (2) yet) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 osa1): I "fixed" (2), but that made some tests that were previously (just (1)) passing fail. Maybe I misunderstood what it's supposed to do. With my fix for (1) currently these tests are failing when running the test suite with `EXTRA_HC_OPTS="-fstatic-argument-transformation -dcore- lint"`: {{{ ManyAlternatives ManyConstructors MultiLayerModules T10370 T10547 T10858 T10989 T12150 T12227 T12234 T12425 T12545 T12707 T13035 T13056 T13143 T13379 T13701 T13719 T13825-ghci T14052 T14683 T14697 T15164 T1969 T2182ghci T3064 T3294 T3591 T4029 T4801 T4945 T5030 T5321FD T5321Fun T5631 T5642 T5837 T6048 T6106 T783 T8353 T8425 T9020 T9233 T9293 T9630 T9675 T9872a T9872b T9872c T9872d T9961 break008 break009 break026 determ017 ghci.prog009 ghci.prog010 ghci024 ghci025 ghci038 ghci057 ghci058 inline-check joao-circular parsing001 print007 prog001 prog002 prog003 prog012 prog013 rule2 spec001 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 osa1): These are all stat failures: (not good enough) - T10858 - T1969 - T3294 - T4801 - T3064 - T5030 - T5631 - parsing001 - T783 - T5321Fun - T5321FD - T5642 - T5837 - T6048 - T9020 - T9675 - T9872a - T9872b - T9872c - T9872d - T9961 - T9233 - T10370 - T10547 - T12227 - T12425 - T12234 - T12545 - T13035 - T13056 - T12707 - T12150 - T13379 - MultiLayerModules - ManyConstructors - ManyAlternatives - T13701 - T13719 - T14697 - T14683 - T9630 - T15164 - T14052 Lint errors: - determ017 - joao-circular - spec001 - T4945 - T13143 - T3591 - T8425 Debug output differs because with this pass we do more inlinings etc. - inline-check - rule2 These are all -fghci-leak-check warnings: - prog001 - prog002 - prog003 - ghci.prog009 - ghci.prog010 - prog012 - prog013 - ghci024 - ghci025 - ghci038 - ghci057 - T2182ghci - T6106 - ghci058 - T8353 - T9293 - T10989 - T13825-ghci - print007 - break008 - break009 - break026 - T4029 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): Crumbs -- code in `SAT.hs` is extremely impenetrable. But it is mainly doing the right thing; the "weird cloning" is nearly right. Here's an example {{{ f :: forall a b. (a,b) -> b -> Int f = /\a b. \(x:(a,b)) (y:b). <body> where <body> is an expression mentioning a, b, x, y and with recursive calls like (f <ty> b <e> y) where presumably <e> :: (<ty>,b) Here the second type argument `b`, and the second value argument `y::b`, are static. The first type arg `a` and value arg `x::(a,b)` are dynamic. The body of `f` may mention any or all of `a`, `b`, `x`, `y`. 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). fwrk a x }}} We must use the ''same'' unique for `f`: we are deliberately shadowing its outer binding. Contrary to the claims in `Note [Binder type capture]` I don't think it matters whether or not we clone the lambda binders; we are free to alpha-rename the lambda as we please, including re-using existing binders. So the bugs seem to be: * In `bindWith` (comment:8) we are abstracting over the type variable, ''but it is static''. This is the real source of the problem. In my example above, note that `b` was static but `a` was not. * Once we fix this we don't need to clone those binders at all; `Note [Binder type capture]` is moot. I also commented on a bug in the Phab. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 osa1):
In bindWith (comment:8) we are abstracting over the type variable, but it is static. This is the real source of the problem. In my example above, note that b was static but a was not.
We introduce two new bindings: - `bindWith_r1` this is the wrapper (or "shadowing" binding). This has to have the exact same type with the original binder (`bindWith`) because it'll shadow the original definition. This has a type arg because the original `bindWith` has one. - `sat_worker_s198` this is the actual worker function without static argument and because all arguments to `bindWith` are static this has no args. So in the actual worker we don't abstract over the static type argument. It seems to me that there isn't a problem with abstracting over static arguments. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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): Phab:D4945 Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * status: patch => new -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14231#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC