GHC plugins don't work on haskell-ide-engine-1.0.0.0

[IchiroKawashima]

trafficstars

Hello,

The problem is the same as #946. I'm working with GHC type checker plugins, just like ghc-typelits-knownnat. hie-0.12.0.0 used to work with those plugins, but neither does hie-1.0.0.0. It seems that hie-1.0.0.0 doesn't recognize the plugins. I hope the IDE engine to give us the same errors as ghc compiler which is used in the project.

I made the following example stack project to demonstrate the problem. I hope the example helps you to figure out the problem. IchiroKawashima/hie-plugins-example

In the project, hie-0.12.0.0 can check types properly by using a GHC plugin but hie-1.0.0.0 gives us an error related types albeit the project can be compiled with stack and its GHC. Note that, all of language extensions and GHC options are described in package.yaml. hie-1.0.0.0 seems to recognize language extensions.

Thank you.

[Avi-D-coder]

I have not used the ghc-typelits-knownnat plugin. I can use RecordDotPreprocessor with hie master. Can you test another plugin?

[IchiroKawashima]

I checked three plugins which handle dependent types:

• GHC.TypeLits.KnownNat.Solver
• GHC.TypeLits.Normalise
• GHC.TypeLits.Extra.Solver

and I couldn't use them with hie-1.0.0.0.

I added examples which couse errors of hie to the example project.

-- • Could not deduce (KnownNat (n + 2))
--     arising from a use of ‘natVal’
--   from the context: KnownNat n
--     bound by the type signature for:
--                knownNatExample :: forall (n :: Nat). KnownNat n => Integer
knownNatExample :: forall (n :: Nat) . (KnownNat n) => Integer
knownNatExample = natVal (Proxy @n) + natVal (Proxy @(n + 2))

-- • Couldn't match type ‘(((4 * x) * ((2 + x) ^ y))
--                         + (4 * ((2 + x) ^ y)))
--                        + (((2 + x) ^ y) * (x ^ 2))’
--                  with ‘(x + 2) ^ (y + 2)’
--   Expected type: Proxy
--                    ((((4 * x) * ((2 + x) ^ y)) + (4 * ((2 + x) ^ y)))
--                     + (((2 + x) ^ y) * (x ^ 2)))
--     Actual type: Proxy ((x + 2) ^ (y + 2))
natNormalizeExample :: forall (x :: Nat) (y :: Nat)
                     . (KnownNat x, KnownNat y)
                    => Proxy ((x + 2) ^ (y + 2))
natNormalizeExample = Proxy :: Proxy (4 * x * (2 + x) ^ y + 4 * (2 + x) ^ y + (2 + x) ^ y * x ^ 2)

-- • Couldn't match type ‘y’ with ‘x ^ Log x y’
--   ‘y’ is a rigid type variable bound by
--     the type signature for:
--       extraExample :: forall (x :: Nat) (y :: Nat).
--                       (KnownNat x, KnownNat y) =>
--                       Proxy (x ^ Log x y)
extraExample :: forall (x :: Nat) (y :: Nat) . (KnownNat x, KnownNat y) => Proxy (x ^ Log x y)
extraExample = Proxy :: Proxy y

hie-0.12.0.0 doesn't couse those errors.