Exception when trying to run compile-time code: substVarsWith: couldn't look up variable substitution

[oofp]

Exception when trying to run compile-time code:
  substVarsWith: couldn't look up variable substitution for res_6341068275337720628

CallStack (from HasCallStack):
error, called at src\Data\Aeson\GADT\TH.hs:131:21 in aeson-gadt-th-0.1.2.0-AuMd3MxiXrSK9OJwKOUSr:Data.Aeson.GADT.TH
Code: deriveJSONGADT ''FlowArrEx
|
1 | {-# LANGUAGE DataKinds #-}
| ^

[ali-abrar]

Hi @oofp could you provide an example datatype that this produces this error? Thanks!

[cgibbard]

I know at least some of the time that error will happen when you provide a type for which the instances don't quite make sense, but it could also be a bug, so it's quite important what your type is. Perhaps we could figure out a better error message to provide.

[oofp]

Thanks @cgibbard and @ali-abrar , I am attaching minimized version of data types (with just few constructors).
MachineArrExSnippet.zip

Please let me know if you want me to try to remove some dependency, so you can actually try to compile it in your environment.

[cgibbard]

Hey, could you try this again with the latest version? There is at least some chance that it will work now, given that we now support data constructors with type class constraints on them (at all).

However, there's still a very strong chance that it won't deal with the functional dependencies correctly, but I can't tell.

[oofp]

Hello,
Now I got:

Exception when trying to run compile-time code:
     substVarsWith: couldn't look up variable substitution for sp_6989586621679116428 with topVars: [q_6989586621679116417,m_6989586621679116418,sp_6989586621679116419,xs_6989586621679116420,xs1_6989586621679116421,ex_6989586621679116422,ex1_6989586621679116423] resultType: AppT (AppT (AppT (AppT (AppT (AppT (AppT (AppT (ConT MachineArrExSnippet.FlowArrEx) (VarT q_6989586621679116431)) (VarT m_6989586621679116426)) (VarT sp_6989586621679116428)) (AppT (AppT PromotedConsT (TupleT 0)) (SigT PromotedNilT (AppT ListT StarT)))) (VarT ol_6989586621679116429)) (SigT PromotedNilT (AppT ListT StarT))) (VarT ex1_6989586621679116430)) (TupleT 0) argType: AppT (AppT (AppT (AppT (AppT (ConT MachineArrExSnippet.ArrStep) (VarT sp_6989586621679116428)) (VarT ol_src_6341068275337765005)) (SigT PromotedNilT (AppT ListT StarT))) (VarT ol_6989586621679116429)) (VarT ex1_6989586621679116430)
CallStack (from HasCallStack):
 error, called at src\Data\Aeson\GADT\TH.hs:215:21 in aeson-gadt-th-0.2.1.0-CGK2EVHBDJDDRySGoPcxtw:Data.Aeson.GADT.TH
   Code: deriveJSONGADT ''FlowArrEx
 |
1 | {-# LANGUAGE DataKinds             #-}
 | ^

[oofp]

Hi again,
Here is minimal example that fails with the same error:

 data SampleGADT (m :: * -> *) (a :: *)   where 
  UnitOK :: SampleGADT m ()
  ReturnIntOK :: Int -> SampleGADT m Int
  --ReturnAErr :: a -> SampleGADT m a

deriveJSONGADT ''SampleGADT 

It compiles with ReturnAErr commented, but when I uncomment this lines I get:

    Exception when trying to run compile-time code:
      substVarsWith: couldn't look up variable substitution for a_6989586621680274059 with topVars: [m_6989586621680274055] resultType: AppT (AppT (ConT MachineArrExSnippet.SampleGADT) (VarT m_6989586621680274060)) (VarT a_6989586621680274059) argType: VarT a_6989586621680274059
CallStack (from HasCallStack):
  error, called at src\Data\Aeson\GADT\TH.hs:215:21 in aeson-gadt-th-0.2.1.0-CGK2EVHBDJDDRySGoPcxtw:Data.Aeson.GADT.TH
    Code: deriveJSONGADT ''SampleGADT
  |
1 | {-# LANGUAGE DataKinds             #-}

[srid]

I wonder if this is the same issue:

-- | View operations for `PropertyGraph`
data PropertyGraphView v vp ep r where
  PropertyGraphView_All :: PropertyGraphView v vp ep (PropertyGraph vp ep v)
  PropertyGraphView_GetVertexProperty :: GCompare vp => v -> vp a -> PropertyGraphView v vp ep (Maybe a)
  PropertyGraphView_GetEdgeProperty :: GCompare ep => v -> v -> ep a -> PropertyGraphView v vp ep (Maybe a)

The last two constructors fail (due to vp a and ep a in arguments) with:

    Exception when trying to run compile-time code:
      substVarsWith: couldn't look up variable substitution for a_6341068275337742300 with topVars: [v_6989586621679093714,vp_6989586621679093715,ep_6989586621679093716] resultType: AppT (AppT (AppT (AppT (ConT Data.PropertyGraph.PropertyGraphView) (VarT             
v_6989586621679093722)) (VarT vp_6989586621679093721)) (VarT ep_6989586621679093724)) (AppT (ConT GHC.Base.Maybe) (VarT 
a_6341068275337742300)) argType: AppT (VarT vp_6989586621679093721) (VarT a_6341068275337742300)

[3noch]

For ReturnAErr :: a -> SampleGADT m a how would it know how to encode/decode a to/from JSON? Does changing this to ReturnAErr :: (ToJSON a, FromJSON a) => a -> SimpleGADT m a help?

[3noch]

Similarly, there is no evidence that vp a and ep a can be (de)serialized into JSON.

[srid]

@3noch Shouldn't this library automatically add those constraints in the JSON instances it generates? Adding them, instead, to the GADT constructors actually has no effect on the substVarsWith error.

[srid]

Also I'm forced to use vp a (instead of say Some vp - which would actually resolve this) in order to unify the a in last parameter Maybe a with the a in the constructor argument vp a.

[3noch]

@srid In your constructor there is an implicit forall v vp a. Since v and vp show up in the type on the far right, you can add constraints to it "outside" of the constructor. But any type that does not show up there, is effectively existentially quantified (just as with Some). Those types are a and vp a which are not directly parameters of your type and so cannot have constraints added by TH. This is even more obvious when you realize that you are specifying GCompare constraints inside the constructor.

EDIT: Well actually a is a parameter to your type, under the Maybe so you could constrain it, which should be enough to get this working.

[3noch]

I suppose this library could, in theory, use ToJSON1/FromJSON1 on vp directly? @cgibbard? That might be really tricky though, as you'd have to detect the arity of all type parameters.

[3noch]

However, @srid, your point does resolve my question for @oofp's problem. That has nothing tricky going on so it should work.

[3noch]

Haha, now I see from the examples in the README that it works with DSum and as you said, Some. So this is more confusing than I first imagined. I'll just shut up and let someone who understands this library chime in. 😊

[3noch]

@cgibbard The minimal repro case is actually:

data SampleGADT :: * -> * where
  ReturnAErr :: a -> SampleGADT a

[3noch]

However, very strangely, this works:

data SampleGADT c a where
  ReturnAErr :: c -> SampleGADT c a

[3noch]

It seems it has trouble adding constraints to the very last argument of the type?

[3noch]

Indeed the last argument is explicitly dropped via init in

aeson-gadt-th/src/Data/Aeson/GADT/TH.hs

Line 70 in cd738fa

(matches, constraints') <- runWriterT (mapM (fmap pure . conMatchesToJSON opts (init topVars)) cons)

and elsewhere.

[chrisdone]

Just FYI I also tried this library out and got:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
module T where

import Data.Aeson.GADT.TH

data Expr a where
  IfE :: Expr Bool -> Expr a -> Expr a -> Expr a
  ListE :: [Expr a] -> Expr [a]
  PureE :: a -> Expr a

deriveJSONGADT ''Expr

     Exception when trying to run compile-time code:
       substVarsWith: couldn't look up variable substitution for a_6989586621679046018 with topVars: [] resultType: AppT (ConT T.Expr) (VarT a_6989586621679046018) argType: AppT (ConT T.Expr) (VarT a_6989586621679046018)

[cgibbard]

For any case where you think it should generate an instance, it would be really good if you could write one by hand for me to be able to understand what code it is that you'd like the TH to generate.

I know there are a few deficiencies, but remember that it's writing an instance of FromJSON (Some (MyType a_1 a_2 ... a_(n-1))) for you -- leaving the last variable out. So if that variable needs to be constrained in some way, there's nowhere to put the constraint.

Also, if pattern matching on other arguments to your data constructor won't determine the type of something we need to FromJSON, you're generally going to be hosed.

In the case of ReturnAErr / PureE above, at what type should parseJSON be applied to parse the argument, in the Some SampleGADT / Some Expr instances?

Of course, there is a real bug here: the error message really sucks, and I apologise for that. It would be good to figure out various things we can do to maybe produce a more informative one.

[chrisdone]

I ended up with a manual instance using Typeable https://gist.github.com/chrisdone/5f584fed711299a1312f87b236d7df59 I'm not sure whether there is an automated way to work with this kind of GADT or not.

[cgibbard]

I don't currently have code which checks for Typeable instances in resolving stuff like this, but it would be a possible thing to do. The trick with "OK" in that code there is probably harder to support though. Another way to factor things would be to use something like:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}

import Data.Aeson.GADT.TH

data OK a where
  OK_Int :: OK Int
  OK_String :: OK String
  OK_Bool :: OK Bool
  OK_Expr :: OK a -> OK (Expr a)

data Expr a where
  IfE :: Expr Bool -> Expr a -> Expr a -> Expr a
  ListE :: OK a -> [Expr a] -> Expr [a]
  PureE :: OK a -> a -> Expr a
  (:=) :: Expr a -> Expr a -> Expr Bool
  LengthE :: Expr [Double] -> Expr Int

deriveJSONGADT ''OK
deriveJSONGADT ''Expr

However, generating the instance for OK presently fails with a similar error message, and that one I don't think should be an issue, and which I'm fairly certain was working at some point in the past. The generated instance should look something like this:

instance ToJSON (OK a) where
  toJSON OK_Int = toJSON ("OK_Int", ())
  toJSON OK_String = toJSON ("OK_String", ())
  toJSON OK_Bool = toJSON ("OK_Bool", ())
  toJSON (OK_Expr x) = toJSON ("OK_Expr", toJSON x)

instance FromJSON (Some OK) where
  parseJSON v = do
    (tag,x) <- parseJSON v
    case tag of
      "OK_Int" -> return (Some OK_Int)
      "OK_String" -> return (Some OK_String)
      "OK_Bool" -> return (Some OK_Bool)
      "OK_Expr" -> do
        Some y <- parseJSON x
        return (Some (OK_Expr y))

Hopefully the changes I've started working on to make the various bits of GADT-related TH we use more robust will eventually fix that en passant (as soon as I can pop them off my stack and finish them).

Trying it by hand, I'm not 100% sure how to make the parser for ListE go through mechanically though... hmm.