Having trouble creating an extension that produces union values

[1chb]

For me it is not obvious which Expr constructor to use for union values, but ghci revealed that it probably should be Field, and embed inject A confirms that. But I just can't get it to work. Here is my code:

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE OverloadedStrings #-}

module ExtensionTest (test) where

import qualified Data.Text as T
import Data.Void (Void)
import Dhall (FromDhall, ToDhall)
import qualified Dhall
import qualified Dhall.Context
import qualified Dhall.Core as DCore
import qualified Dhall.Map as DMap
import Dhall.Marshal.Encode (embed, inject)
import qualified Dhall.Parser as DParser
import GHC.Generics (Generic)
import qualified Lens.Family as Lens

data ABC = A | B | C
  deriving stock (Generic, Show)
  deriving anyclass (FromDhall, ToDhall)

abcDecoder :: Dhall.Decoder ABC
abcDecoder = Dhall.auto

abcType :: DCore.Expr DParser.Src Void
abcType = maximum $ Dhall.expected abcDecoder

test :: IO ()
test = do
  let startingContext = abcId $ abcShow $ abcLow Dhall.Context.empty
        where
          abcLow = Dhall.Context.insert "ABC/low" abcType
          abcShow = Dhall.Context.insert "ABC/show" (DCore.Pi Nothing "_" abcType DCore.Text)
          abcId = Dhall.Context.insert "ABC/id" (DCore.Pi Nothing "_" abcType abcType)

  let abcType' = DCore.Union $ DMap.fromList [("A", Nothing), ("B", Nothing), ("C", Nothing)]
      abcLowValue = DCore.Field abcType' $ DCore.FieldSelection Nothing "A" Nothing
  let normalizer :: MonadFail f => DCore.Expr s Void -> f (DCore.Expr s Void)
      normalizer (DCore.Var "ABC/low") =
        -- pure $ embed inject A
        pure abcLowValue
      normalizer (DCore.App (DCore.Var "ABC/show") expr) =
        let debug = case embed inject A of
              DCore.Field (DCore.Union dmap) (DCore.FieldSelection _ t _) ->
                " {-Field=" <> t <> ", " <> T.pack (show $ DMap.toList dmap) <> "-}"
              _ -> "Something else"
            unpack (k, Nothing) = (T.unpack k, Nothing :: Maybe ())
            unpack _ = ("?", Just ())
            debug2 = case abcLowValue of
              DCore.Field (DCore.Union dmap) (DCore.FieldSelection _ t _) ->
                " {-Field=" <> t <> ", " <> T.pack (show $ unpack <$> DMap.toList dmap) <> "-}"
              _ -> "Something else"
        in pure $ DCore.TextLit $ DCore.Chunks [] $ DCore.pretty expr <> debug <> debug2
      normalizer (DCore.App (DCore.Var "ABC/id") expr) =
        pure expr
      normalizer expr = fail $ T.unpack $ "normalizer: " <> DCore.pretty expr

  let inputSettings = transform Dhall.defaultInputSettings
        where
          transform =
            Lens.set Dhall.normalizer (Just (DCore.ReifiedNormalizer $ pure . normalizer))
              . Lens.set Dhall.startingContext startingContext

  let text =
        "let ABC = < A | B | C > \
        \ let r1 = ABC/low \
        \ let r2 = ABC/id ABC.B \
        \ let r3 = ABC/show ABC.C \
        \ in {r1 = r2, r2 = r2, r3 = r3}"

  x <- Dhall.inputWithSettings inputSettings Dhall.auto text :: IO Result
  print x

data Result = Result {r1 :: ABC, r2 :: ABC, r3 :: T.Text }
  deriving stock (Generic, Show)
  deriving anyclass (FromDhall, ToDhall)

Running this gives:

Result
 { r1 = B
 , r2 = B
 , r3 = "< A | B | C >.C
          {-Field=A, [(\"A\",Nothing),(\"B\",Nothing),(\"C\",Nothing)]-}
          {-Field=A, [(\"A\",Nothing),(\"B\",Nothing),(\"C\",Nothing)]-}"
 }

But the value of r1 is not correct, because I put r1 = r2 in the result of the test program, so my extension function ABC/low was not used. Also note that r3 confirms that embed inject A builds the same Expr as ABC/low. If I instead put r1 = r1, as it should be, I get:

Error: Invalid Dhall.Decoder                                               
                                                                                
Every Decoder must provide an extract function that does not fail with a type   
error if an expression matches the expected type.  You provided a Decoder that  
disobeys this contract                                                          
                                                                                
The Decoder provided has the expected dhall type:                               
                                                                                
↳ < A | B | C >
                                                                                
and it threw a type error during extraction from the well-typed expression:     
                                                                                
↳ ABC/low

So why am I not just using (embed . inject) to convert Haskell to Dhall, i.e. pure $ embed inject A? Because it doesn't type check:

• Couldn't match type ‘s’ with ‘DParser.Src’
  Expected: f (DCore.Expr s Void)
    Actual: f (DCore.Expr DParser.Src Void)

This is due to the type signature of normailzer. If I remove it the type error moves to the usage of the normailizer, i.e. Lens.set Dhall.normalizer (Just (DCore.ReifiedNormalizer $ pure . normalizer)):

• Couldn't match type ‘s’ with ‘DParser.Src’
  Expected: DCore.Expr s Void
            -> Lens.Identity (Maybe (DCore.Expr s Void))
    Actual: DCore.Expr DParser.Src Void
            -> Lens.Identity (Maybe (DCore.Expr DParser.Src Void))

This is also the reason why I hard coded abcType' instead of just reusing the generated abcType.

Hopefully I'm doing it wrongly. This neither is convenient or works.

[1chb]

I did some more investigations. Now it seems the problem is that my non-working extension doesn't take an argument. If I add a dummy Natural argument it works. I also tried to create an extension an argument-less function that results in a Text and it also fails:

Error: Invalid Dhall.Decoder                                               
                                                                                
Every Decoder must provide an extract function that does not fail with a type   
error if an expression matches the expected type.  You provided a Decoder that  
disobeys this contract                                                          
                                                                                
The Decoder provided has the expected dhall type:                               
                                                                                
↳ Text
                                                                                
and it threw a type error during extraction from the well-typed expression:     
                                                                                
↳ ABC/text

So my problem is not related to Enum at all.

[Gabriella439]

Side note: you can simplify {r1 = r2, r2 = r2, r3 = r3} to { r1, r2, r3 } in newer versions of Dhall

Yeah, this seems like a bug. I narrowed down the reproduction to this:

{-# LANGUAGE OverloadedStrings #-}

module ExtensionTest where

import Dhall.Core (Expr(..), ReifiedNormalizer(..), Var(..))

import qualified Dhall
import qualified Dhall.Context as Context
import qualified Lens.Family as Lens

main :: IO ()
main = do
  let startingContext = Context.insert "foo" Integer Context.empty

  let normalizer (Var (V "foo" 0)) = Just (IntegerLit 0)

      normalizer _ = Nothing

  let inputSettings = transform Dhall.defaultInputSettings
        where
          transform =
                Lens.set Dhall.normalizer
                    (Just (ReifiedNormalizer $ pure . normalizer))
              . Lens.set Dhall.startingContext startingContext

  x <- Dhall.inputWithSettings inputSettings Dhall.auto "foo" :: IO Integer

  print x

… which still fails with:

ExtensionTest.hs: Error: Invalid Dhall.Decoder                                               
                                                                                
Every Decoder must provide an extract function that does not fail with a type   
error if an expression matches the expected type.  You provided a Decoder that  
disobeys this contract                                                          
                                                                                
The Decoder provided has the expected dhall type:                               
                                                                                
↳ Integer
                                                                                
and it threw a type error during extraction from the well-typed expression:     
                                                                                
↳ foo

What should have happened is that the normalizer should have replaced foo with 0 before decoding the expression and then the decoding would have succeeded. However, for some reason a non-normalized expression is being decoded, which is unexpected. I'm still investigating why this happens.

[1chb]

Thanks for the quick reply. Yes, it seems like a bug. However, I realized that that this approach will not solve my use case. I planned to provide different contexts for different runs, but this approach is not compatible with the caches.

[Gabriella439]

Yeah, I understand.

Regardless, I found the root cause of the bug and the fix is up here: #2464