Dhall-haskell: Decoder.expected does not terminate when datatype uses recursion

[mmhat]

Consider the following Haskell type:

data StringList = Cons String StringList | Nil
    deriving Generic

instance FromDhall StringList

We cannot translate that to Dhall due to the recursive definition and expected (auto :: Decoder StringList) will not terminate.

I propose to add some kind of termination checking to the generic implementation of autoWith and throw an error if the type in question uses a recursive definition.

[Gabriel439]

@mmhat: Actually, we do support FromDhall instances for recursive types via the FromDhall instance for Fix. I believe with a little bit of glue we could reuse that instance to power Generic support for FromDhall for recursive Haskell types

[mmhat]

@Gabriel439 I was not aware of that instance. So the default implementation of autoWith should be something like this?

autoWith options x = if isRecursive x
    then Data.Fix.cata Data.Functor.Foldable.embed <$> ...
    else ...

where ... is the generic implementation we use now. Then the user could use like (referring to the Fix example):

TH.makeBaseFunctor ''Expr
deriving instance Generic (ExprF a)
deriving instance FromDhall a => FromDhall (ExprF a)
instance FromDhall Expr

I managed to implement the isRecursive function using Generics and Data.Typeable for comparison. Which means people must derive a Typeable instance in addition to the Generic one which in turn means we break peoples code and I'm not sure if we want that...

[mmhat]

Follow up: It would require (Corecursive a, FromDhall (Base a (Result (Base a)))) as well which is definitely something we don't want.

[Gabriel439]

@mmhat: There should be a simpler solution for types that derive Generic1 because the Generic1 class includes type-level metadata about whether or not a field is recursive so that you don't need to detect it at the term level. For example:

>>> data List a = Cons a (List a) | Nil deriving (Generic1)
>>> :kind! Rep1 List
Rep1 List :: * -> *
= D1
    ('MetaData "List" "Ghci7" "interactive" 'False)
    (C1
       ('MetaCons "Cons" 'PrefixI 'False)
       (S1
          ('MetaSel
             'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
          Par1
        :*: S1
              ('MetaSel
                 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
              (Rec1 List))
     :+: C1 ('MetaCons "Nil" 'PrefixI 'False) U1)

[mmhat]

I started working on this. My draft is here.
However, note the line 1382 and the following ones which still cause a problem.

[Gabriel439]

@mmhat: Do you need to implement a general Inhabits type family? It might suffice to implement a simpler IsRecursive type family that detects whether or not a Rec1 type parameter is present

[mmhat]

@Gabriel439 The problem with Generic1/Rec1 is that we are unable to detect recursion like the one in the StringList type in my original issue description since one cannot derive Generic1 for monomorphic datatypes.
However, I updated my draft and it seems to work (have a look at line 1382). But I think we do need a thorough review here, preferably by someone who has a deep(er) understanding of closed type families (in presence of UndecidableInstances).
The question is if it is possible to construct a type (in a trivial way, e.g. not something we definitly won't see in the wild anyway) which breaks Inhabits either by yielding a wrong result, letting the type checker loop or being not able to unify the type instance.

[mmhat]

And here it is: data Foo a b = Foo a b (Foo a b) | FooNil
Then Inhabits (Foo a b) (Rep (Foo a b)) ~ 'False.
I wonder how to convince the type checker that i.e. Inhabits (T a) (K1 R a) ~ 'False since this would be an infinite type.

[Gabriel439]

@mmhat: Would it be possible to change that line to:

Inhabits (f x) (K1 R a) = Inhabits f (K1 R a) || Inhabits x (K1 R a)

[mmhat]

@Gabriel439 Unfortunately, no. Using

test :: Proxy (Inhabits (Foo a b) (Rep (Foo a b)))
test = Proxy

fails with

Couldn't match type ‘(Inhabits a0 (K1 R a0) ...
...
Expected type: Proxy (Inhabits (Foo a b) (Rep (Foo a b)))
Actual type: Proxy (Inhabits (Foo a0 b0) (Rep (Foo a0 b0)))
NB: ‘||’ is a non-injective type family
The type variables ‘a0’, ‘b0’ are ambiguous

GHC suggests AllowAmbiguousTypes but with those instance (FromDhall a, FromDhall b) => FromDhall (a, b) fails with

Could not deduce (GDecoder (a, b) ((Inhabits a (K1 R a)  || Inhabits b (K1 R a)) || (Inhabits a (K1 R b) || Inhabits b (K1 R b))))

[mmhat]

I especially wonder why Inhabits (a, b) (K1 R (a, b)) is not a match for the instance Inhabits a (K1 R a) = 'True.

[Gabriel439]

@mmhat: One thing I noticed is that your definition for || has overlapping cases:

type family a || b :: Bool where
    'False || b = b
    'True  || b = 'True
    a || 'False = a
    a || 'True  = 'True

... and I think the overlap is confusing the type checker. Try changing it to:

type family a || b :: Bool where
    'False || 'False = 'False
    'True  || 'False = 'True
    'False || 'True = 'True
    'True || 'True  = 'True

[mmhat]

@Gabriel439 No success: Fails with the same errors.

[Gabriel439]

@mmhat: What if you also make it injective and annotate the arguments to be of type Bool: https://gitlab.haskell.org/ghc/ghc/wikis/injective-type-families

This is where I'm reaching the limits of what I know about type families since I've never used them before

[mmhat]

@Gabriel439 Unfortunately those type families are indeed not injective. I updated my working branch once more an at least it works for recursive types without type variables.
Generic instances for recursive types with type variables won't compile anymore.
Have a look at the assertions starting at line 151 of the new Dhall.TypeLevel module and this module in general.
I have to admit that I reached my limit as well. Maybe someone else in the community comes up with a better solution.

[sjakobi]

As long as we can't get the decoding right, it would be nice if we could produce a proper error at runtime or ideally compile time, instead of simply looping until users run out memory (https://github.com/dhall-lang/dhall-haskell/issues/1691).

[mmhat]

Yeah, I guess that's the way to go - at least for the moment. I'd still like to see a "proper" solution for this problem. I had to pause my work on this issue but I'll continue in about two weeks or so. I'd like to proceed as follows:

1. Detect recursion at runtime and throw an exception. Update the documentation and add a big warning sign to the tutorial.

2. Add support for simple recursive types. For example types where the type constructor is mentioned in the data constructor, e.g. data Foo = Foo Text Foo. Maybe use the recursion detection from step one to generate the correct Dhall type at runtime?

3. Explore some more advanced methods like the one I tried in order to minimize the runtime overhead.

[mmhat]

I started working on this issue again and I'm stuck with some overlapping instances.
Interestingly GHCi compiles without complaining but when I try to build it with stack the program is rejected.
The current working branch can be found here.

I really start to wonder if this issue can be resolved using only Generics and without imposing further constraints on the GenericFromDhall type class.

Another idea:
Change the Decoder.expected from Expr Src Void to Expr Src Void -> Bool or something like that and during type checking feed the type signature in question to that function and let the decoder decide whether it's appropriate. But I really don't know enough about the theoretical foundation of Dhall and hence I don't know if this is sound.

cc @Gabriel439

[Gabriel439]

@mmhat: I don't think changing the type of Decoder.expected would work as people currently use that to generate Dhall types from Haskell types in order to keep the two in sync.

However, it's fine to use error for now to signal unexpected recursion since it would be no worse than the current behavior (an infinite loop)

[mmhat]

@Gabriel439 I expected that. However, whether to use error or not is not the difficult part. The problem is that we don't have a notion of equality: Right now I pass a Proxy a through the whole GenericFromDhall machinery (Have a look at the changed class signature of GenericFromDhall.) with a being the type we want to check for recursion. But I suspect that the current approach leveraging overlapping instances might be to fragile. I ran into some issues with that when I tried to solve this issue the first time and right now the test I provide (checking data RecursiveType = RecursiveType RecursiveType) fails due to GHC having difficulties to determine the instance to use.

Generics are of no use here since the name of the type constructor is encoded as a type level string which cannot be compared to types in the data constructors unless we impose a Generic constraint on those (which is really bad).

I'm inclined to bite the bullet and put a Typeable constraint on GenericFromDhall which will allow us to compare types in a sane way...

[Gabriel439]

@mmhat: Yeah, I think a Typeable constraint should probably be fine, especially since Haskell types now automatically derive Typeable, so it's not a disruptive change

[mmhat]

Did it without an additional Typeable constraint. :smile:

[mmhat]

Fixed in https://github.com/dhall-lang/dhall-haskell/commit/6bf8959e77383a3d1302e5e0212c27aaf75637a4. by merging https://github.com/dhall-lang/dhall-haskell/pull/1825.
Closing.