Tactic plugin: Excludes Dictionary arguments in GADTs in Destruct Tactic

[konn]

Consider the following:

{-# LANGUAGE GADTs #-}
module GoldenGADTDestruct where
data CtxGADT where
  MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT

ctxGADT :: CtxGADT -> String
ctxGADT gadt = _decons

If we select case split on gadt at _decons, the Tactic Plugin in HEAD introduces instance dictionary in data constructor:

{-# LANGUAGE GADTs #-}
module T4 where
data CtxGADT where
  MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT

ctxGADT :: CtxGADT -> Bool
ctxGADT gadt = (case gadt of { (MkCtxGADT sa ea a) -> _ })

As it stands, generated pattern includes dictionary argumetns, which must not (cannot) appear in the source language.
This behaviour is due to the call to the dataConInstArgTys, which also includes dictionary argument.
This pull-request changes to use dataConInstOrigArgTys, which excludes dictionaries and adds a golden test for destructing GADTs, and the above case-splitting generates the expected result:

ctxGADT :: CtxGADT -> Bool
ctxGADT gadt = (case gadt of { (MkCtxGADT a) -> _ })

One concern: I also change the use of dataConInstArgTys in buildDataCon to dataConInstOrigArgTys. This should also correct the expression constructed by Homo or Auto tactic, but the generated expressions don't take type-level constraints into account. Any thoughts?

[alanz]

cc @isovector @TOTBWF

[konn]

OMG it hangs with >= 8.8...

[konn]

I introduced the variant of dataConInstArgTys which excludes isClassTyCon after wards.
It seems still failing in 8.10.2, but it is due to dependency issue?

[jneira]

Yeah data-tree-print-0.1.0.2 should be added to stack-8.10.2.yaml to make it work

[konn]

Ok, it seems all CI passed!

[isovector]

Looks great! Thanks so much, @konn!