agda2hs inlines function with explicit forall but not without

[jespercockx]

Here is a minimal example of the issue reported by @HeinrichApfelmus in #366 (comment):

open import Haskell.Prelude

member : ∀ {a : Set} {{_ : Ord a}} → a → a
member w = w

prune : {{_ : Ord a}} → a → a
prune w = member w

{-# COMPILE AGDA2HS member #-}
{-# COMPILE AGDA2HS prune #-}

This is compiled to

member :: Ord a => a -> a
member w = w

prune :: Ord a => a -> a
prune w = w

However, removing the ∀ {a : Set} from the type of member produces the non-inlined version

prune w = member w

Looking at the debug output, this is actually the fault of agda2hs, not of agda itself:

compiling clause:  <unnamedclause> w = member w
[...]
compiling term: member w
Reached variable

[jespercockx]

Once again, the culprit is the projection-like optimization: using --no-projection-like makes the problem disappear. So Agda is (partially) to blame after all: why does it recognize member as being projection-like when an explicit quantification is used, but not when a is a generalized variable? (I reported this upstream as agda/agda#7530)