Skip to content

Split correctly on datatypes with existential type variables #32

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
WorldSEnder opened this issue Oct 16, 2020 · 4 comments · Fixed by haskell/haskell-language-server#508

Comments

@WorldSEnder
Copy link

WorldSEnder commented Oct 16, 2020

{-# 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 79b98f0 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
Copy link

konn commented Oct 17, 2020

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
Copy link

konn commented Oct 17, 2020

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

@konn
Copy link

konn commented Nov 23, 2020

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
Copy link
Owner

We found a bug in github!

isovector pushed a commit that referenced this issue Dec 23, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants