Split correctly on datatypes with existential type variables

[WorldSEnder]

{-# LANGUAGE GADTs, RankNTypes #-}

data E a b where
  E :: forall a b. (b ~ a, Ord a) => b -> E a [a]

test :: E Int b -> Int
test x = _

In the above, case splitting on x will result in

test x = (case x of { (E stltlbl_i b) -> _ })

which introduces an additional argument to E that should not be there. My suspicion is that this was introduced with 79b98f000c090872c75152557d540dc5c19f1385 which is the opposite of what I'd expect from the commit message.

Can you shed more light on what issue the commit was fixing @konn ? Replacing dataConInstArgTys with dataConInstOrigArgTys seems to work fine with ghc 8.6.5 and also works with the above test case.

[konn]

Thanks for pointing it out! Aha, so we must exclude isCoercionTyCon as well. dataConInstArgTys cannot be used here, since, as stated in haddock, it also includes dictionary arguments (i.e. instance except for coercions) which must be excluded as well. It doesn't include dictionaries for a 〜 b because it is treated differencely with class dictionaries (e.g. Ord a, which is excluded from the arguments correctly here).(EDIT: the preceding sentence was incorrect. please ignore) So, if I understand Haddock correctly, what we must use instead of dataConInstOrigArgTys' here should be dataConInstOrigArgTys as you suggested; but, at least when I made a pull-request, it paniced mysteriously on some versions of GHC when CI was run. Hence we are just doing some filtering to the raw data args obtained by dataConInstArgTys for now, and we need extra filtering to exclude coercion arguments as well.

I will make another pull-req. shortly. Thank you again for a catch!

[konn]

Since this can be independently fixed on the original branch, I filed the pull-request in the haskell/haskell-language-server as haskell/haskell-language-server#508.

[konn]

I assume this issue is accidentally closed by GitHub (b/c the commit message closing this issue doesn't change anything related to tactics plugin at all!), and the bug itself still persists both in haskell/haskell-language-server and this repository, right?

And I think my pull-req haskell#508 can finally fix this isuue. @isovector @WorldSEnder Would you take a look at this PR, please?

[isovector]

We found a bug in github!