QuickCheck.hs

-- TODO: update because we added ShowConstructor constructor to Expr in Dhall.Syntax

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE ViewPatterns        #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

-- Build without optimizations to prevent out-of-memory situations in Hydra CI
{-# OPTIONS_GHC -O0 #-}

module Dhall.Test.QuickCheck where

import Data.Either            (isRight)
import Data.Either.Validation (Validation (..))
import Data.Text              (Text)
import Data.Void              (Void)
import Dhall
    ( FromDhall (..)
    , ToDhall (..)
    , Vector
    , auto
    , embed
    , extract
    , inject
    )
import Dhall.Core
    ( Binding (..)
    , Chunks (..)
    , Const (..)
    , DhallDouble (..)
    , Directory (..)
    , Expr (..)
    , FieldSelection (..)
    , File (..)
    , FilePrefix (..)
    , FunctionBinding (..)
    , Import (..)
    , ImportHashed (..)
    , ImportMode (..)
    , ImportType (..)
    , PreferAnnotation (..)
    , RecordField (..)
    , Scheme (..)
    , URL (..)
    , Var (..)
    , WithComponent (..)
    )
import Dhall.Map              (Map)

import Data.Functor.Identity     (Identity (..))
import Data.Proxy                (Proxy (..))
import Data.Typeable             (Typeable, typeRep)
import Dhall.Parser              (Header (..), createHeader)
import Dhall.Pretty              (CharacterSet (..))
import Dhall.Set                 (Set)
import Dhall.Src                 (Src (..))
import Dhall.Test.Format         (format)
import Dhall.TypeCheck           (TypeError, Typer)
import Generic.Random            (ConstrGen (..), W, Weights, (%), (:+) (..))
import Test.QuickCheck
    ( Arbitrary (..)
    , Gen
    , NonNegative (..)
    , Positive (..)
    , Property
    , genericShrink
    , suchThat
    , (===)
    , (==>)
    )
import Test.QuickCheck.Instances ()
import Test.Tasty                (TestTree)
import Test.Tasty.QuickCheck     (QuickCheckTests (..))
import Text.Megaparsec           (Pos, SourcePos (..))

import qualified Control.Spoon
import qualified Data.Char
import qualified Data.Foldable         as Foldable
import qualified Data.HashMap.Strict   as HashMap
import qualified Data.HashSet
import qualified Data.List
import qualified Data.Map
import qualified Data.Sequence
import qualified Data.Set
import qualified Data.SpecialValues
import qualified Data.Text             as Text
import qualified Data.Time             as Time
import qualified Dhall.Binary
import qualified Dhall.Context
import qualified Dhall.Core
import qualified Dhall.Diff
import qualified Dhall.Map
import qualified Dhall.Parser          as Parser
import qualified Dhall.Set
import qualified Dhall.TypeCheck
import qualified Generic.Random
import qualified Lens.Micro            as Lens
import qualified Numeric.Natural       as Nat
import qualified Test.QuickCheck
import qualified Test.Tasty
import qualified Test.Tasty.QuickCheck
import qualified Text.Megaparsec       as Megaparsec

instance (Arbitrary a, Ord a) => Arbitrary (Set a) where
  arbitrary = Dhall.Set.fromList <$> arbitrary
  shrink = map Dhall.Set.fromList . shrink . Dhall.Set.toList

lift0 :: a -> Gen a
lift0 = pure

lift1 :: Arbitrary a => (a -> b) -> Gen b
lift1 f = f <$> arbitrary

lift2 :: (Arbitrary a, Arbitrary b) => (a -> b -> c) -> Gen c
lift2 f = f <$> arbitrary <*> arbitrary

lift3 :: (Arbitrary a, Arbitrary b, Arbitrary c) => (a -> b -> c -> d) -> Gen d
lift3 f = f <$> arbitrary <*> arbitrary <*> arbitrary

lift4
    :: (Arbitrary a, Arbitrary b, Arbitrary c, Arbitrary d)
    => (a -> b -> c -> d -> e) -> Gen e
lift4 f = f <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary

lift5
    :: ( Arbitrary a
       , Arbitrary b
       , Arbitrary c
       , Arbitrary d
       , Arbitrary e
       )
    => (a -> b -> c -> d -> e -> f) -> Gen f
lift5 f =
      f <$> arbitrary
        <*> arbitrary
        <*> arbitrary
        <*> arbitrary
        <*> arbitrary

lift6
    :: ( Arbitrary a
       , Arbitrary b
       , Arbitrary c
       , Arbitrary d
       , Arbitrary e
       , Arbitrary f
       )
    => (a -> b -> c -> d -> e -> f -> g) -> Gen g
lift6 f =
      f <$> arbitrary
        <*> arbitrary
        <*> arbitrary
        <*> arbitrary
        <*> arbitrary
        <*> arbitrary

integer :: (Arbitrary a, Num a) => Gen a
integer =
    Test.QuickCheck.frequency
        [ (7, arbitrary)
        , (1, fmap (\x -> x + (2 ^ (64 :: Int))) arbitrary)
        , (1, fmap (\x -> x - (2 ^ (64 :: Int))) arbitrary)
        ]

whitespace :: Gen Text
whitespace = do
      let commentChar =
              Test.QuickCheck.frequency
                  [ (20, Test.QuickCheck.elements [' ' .. '\DEL'])
                  , ( 1, arbitrary)
                  ]

          noInteriorBlockComments text =
              not (Text.isInfixOf "{-" text || Text.isInfixOf "-}" text)

          commentText =
              suchThat
                  (Text.pack <$> Test.QuickCheck.listOf commentChar)
                  noInteriorBlockComments

          multiline = do
              txt <- commentText
              pure $ "{-" <> txt <> "-}"

          singleline = do
              txt <- commentText `suchThat` (not . Text.isInfixOf "\n")
              endOfLine <- Test.QuickCheck.elements ["\n", "\r\n"]
              pure $ "--" <> txt <> endOfLine

          newlines = Text.concat <$> Test.QuickCheck.listOf (pure "\n")

      comments <- do
          n <- Test.QuickCheck.choose (0, 2)
          Test.QuickCheck.vectorOf n $ Test.QuickCheck.oneof
              [ multiline
              , singleline
              , newlines
              ]

      pure $ Text.unlines comments

shrinkWhitespace :: Text -> [Text]
shrinkWhitespace "" = []
shrinkWhitespace _  = [""]

instance Arbitrary CharacterSet where
    arbitrary = Test.QuickCheck.elements [ ASCII, Unicode ]

instance Arbitrary Header where
    arbitrary = createHeader <$> whitespace

    shrink (Header text) = Header <$> shrinkWhitespace text

instance (Arbitrary v) => Arbitrary (Map Text v) where
    arbitrary = do
        n   <- Test.QuickCheck.choose (0, 2)
        kvs <- Test.QuickCheck.vectorOf n ((,) <$> label <*> arbitrary)
        -- Sorting the fields here because serialization needs them in order
        return (Dhall.Map.fromList (Data.List.sortOn fst kvs))

    shrink =
            map Dhall.Map.fromList
        .   shrink
        .   Dhall.Map.toList

instance (Arbitrary s, Arbitrary a) => Arbitrary (Binding s a) where
    arbitrary = do
        bindingSrc0 <- arbitrary

        variable <- Test.QuickCheck.oneof [ pure "_", label ]

        bindingSrc1 <- arbitrary

        annotation <- arbitrary

        bindingSrc2 <- arbitrary

        value <- arbitrary

        return Binding{..}

    shrink = genericShrink

instance (Arbitrary s, Arbitrary a) => Arbitrary (Chunks s a) where
    arbitrary = do
        n <- Test.QuickCheck.choose (0, 2)
        Chunks <$> Test.QuickCheck.vectorOf n arbitrary <*> arbitrary

    shrink = genericShrink

instance Arbitrary Const where
    arbitrary = Test.QuickCheck.oneof [ pure Type, pure Kind, pure Sort ]

    shrink = genericShrink

instance Arbitrary DhallDouble where
    arbitrary = fmap DhallDouble (Test.QuickCheck.oneof [ arbitrary, special ])
      where
        special = Test.QuickCheck.elements Data.SpecialValues.specialValues

    shrink = genericShrink

instance Arbitrary Directory where
    arbitrary = lift1 Directory

    shrink = genericShrink

instance Arbitrary PreferAnnotation where
    arbitrary = Test.QuickCheck.oneof
        [ pure PreferFromSource
        , pure PreferFromCompletion
        ]

    shrink = genericShrink

instance (Arbitrary s, Arbitrary a) => Arbitrary (RecordField s a) where
    arbitrary = lift4 RecordField

    shrink = genericShrink

instance (Arbitrary s, Arbitrary a) => Arbitrary (FunctionBinding s a) where
    arbitrary = do
        l <- label
        type_ <- arbitrary
        return $ FunctionBinding Nothing l Nothing Nothing type_

    shrink = genericShrink

instance Arbitrary s => Arbitrary (FieldSelection s) where
    arbitrary = FieldSelection <$> pure Nothing <*> label <*> pure Nothing
    shrink = genericShrink

instance Arbitrary WithComponent where
    arbitrary =
        Test.QuickCheck.oneof [ pure WithQuestion, WithLabel <$> arbitrary ]

instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where
    arbitrary =
        Test.QuickCheck.suchThat
            (Generic.Random.withBaseCase
                (Generic.Random.genericArbitraryRecG customGens weights)
                (Var <$> arbitrary)
                )
            standardizedExpression
      where
        customGens
            :: ConstrGen "Lam" 1 (FunctionBinding s a)
            :+ ConstrGen "Pi" 1 Text
            :+ ConstrGen "Field" 1 (FieldSelection s)
            :+ ConstrGen "Project" 1 (Either [Text] (Expr s a))
            :+ Gen Integer  -- Generates all Integer fields in Expr
            :+ Gen Text     -- Generates all Text fields in Expr
            :+ ()
        customGens =
               ConstrGen arbitrary
            :+ ConstrGen label
            :+ ConstrGen arbitrary
            :+ ConstrGen projection
            :+ integer
               -- 'Lam's and 'Pi's are encoded differently when the binding is
               -- the special string "_", so we generate some of these strings
               -- to improve test coverage for these code paths.
            :+ Test.QuickCheck.oneof [pure "_", arbitrary]
            :+ ()

        projection =
            Test.QuickCheck.oneof
                [ fmap Left (Test.QuickCheck.listOf label)
                , arbitrary
                ]

        -- These weights determine the frequency of constructors in the generated
        -- Expr.
        -- They will fail to compile if the constructors don't appear in the order
        -- in which they are defined in 'Expr'!
        weights :: Weights (Expr s a)
        weights =
              (7 :: W "Const")
            % (7 :: W "Var")
            % (7 :: W "Lam")
            % (7 :: W "Pi")
            % (7 :: W "App")
            % (7 :: W "Let")
            % (1 :: W "Annot")
            % (1 :: W "Bool")
            % (7 :: W "BoolLit")
            % (1 :: W "BoolAnd")
            % (1 :: W "BoolOr")
            % (1 :: W "BoolEQ")
            % (1 :: W "BoolNE")
            % (1 :: W "BoolIf")
            % (1 :: W "Bytes")
            % (1 :: W "BytesLit")
            % (1 :: W "Natural")
            % (7 :: W "NaturalLit")
            % (1 :: W "NaturalFold")
            % (1 :: W "NaturalBuild")
            % (1 :: W "NaturalIsZero")
            % (1 :: W "NaturalEven")
            % (1 :: W "NaturalOdd")
            % (1 :: W "NaturalToInteger")
            % (1 :: W "NaturalShow")
            % (1 :: W "NaturalSubtract")
            % (1 :: W "NaturalPlus")
            % (1 :: W "NaturalTimes")
            % (1 :: W "Integer")
            % (7 :: W "IntegerLit")
            % (1 :: W "IntegerClamp")
            % (1 :: W "IntegerNegate")
            % (1 :: W "IntegerShow")
            % (1 :: W "IntegerToDouble")
            % (1 :: W "Double")
            % (7 :: W "DoubleLit")
            % (1 :: W "DoubleShow")
            % (1 :: W "Text")
            % (1 :: W "TextLit")
            % (1 :: W "TextAppend")
            % (1 :: W "TextReplace")
            % (1 :: W "TextShow")
            % (1 :: W "Date")
            % (1 :: W "DateLiteral")
            % (1 :: W "DateShow")
            % (1 :: W "Time")
            % (1 :: W "TimeLiteral")
            % (1 :: W "TimeShow")
            % (1 :: W "TimeZone")
            % (1 :: W "TimeZoneLiteral")
            % (1 :: W "TimeZoneShow")
            % (1 :: W "List")
            % (1 :: W "ListLit")
            % (1 :: W "ListAppend")
            % (1 :: W "ListBuild")
            % (1 :: W "ListFold")
            % (1 :: W "ListLength")
            % (1 :: W "ListHead")
            % (1 :: W "ListLast")
            % (1 :: W "ListIndexed")
            % (1 :: W "ListReverse")
            % (1 :: W "Optional")
            % (7 :: W "Some")
            % (1 :: W "None")
            % (1 :: W "Record")
            % (7 :: W "RecordLit")
            % (1 :: W "Union")
            % (7 :: W "Combine")
            % (1 :: W "CombineTypes")
            % (7 :: W "Prefer")
            % (7 :: W "RecordCompletion")
            % (1 :: W "Merge")
            % (1 :: W "ToMap")
            % (1 :: W "ShowConstructor")
            % (7 :: W "Field")
            % (7 :: W "Project")
            % (1 :: W "Assert")
            % (1 :: W "Equivalent")
            % (1 :: W "With")
            % (0 :: W "Note")
            % (7 :: W "ImportAlt")
            % (7 :: W "Embed")
            % ()

    shrink expression = filter standardizedExpression (genericShrink expression)

standardizedExpression :: Expr s a -> Bool
standardizedExpression (ListLit  Nothing  xs) =
    not (Data.Sequence.null xs)
standardizedExpression (ListLit (Just _ ) xs) =
    Data.Sequence.null xs
standardizedExpression (Note _ _) =
    False
standardizedExpression (Combine _ (Just _) _ _) =
    False
standardizedExpression With{} =
    False
standardizedExpression (Prefer _ PreferFromCompletion _ _) =
    False
-- The following three expressions are valid ASTs, but they can never be parsed,
-- because the annotation will associate with `Merge`/`ListLit`/`ToMap` with
-- higher precedence
standardizedExpression (Annot (Merge _ _ Nothing) _) =
    False
standardizedExpression (Annot (ListLit Nothing _) _) =
    False
standardizedExpression (Annot (ToMap _ Nothing) _) =
    False
standardizedExpression (TimeZoneLiteral (Time.TimeZone _ b t)) =
    not b && null t
standardizedExpression (TimeLiteral (Time.TimeOfDay _ _ ss) precision) =
    isInteger (ss * magnitude)
  where
    magnitude = 10 ^ precision

    isInteger x = x == fromInteger (round x)
standardizedExpression _ =
    True

chooseCharacter :: (Char, Char) -> Gen Char
chooseCharacter = Test.QuickCheck.chooseEnum

instance Arbitrary File where
    arbitrary = lift2 File

    shrink = genericShrink

instance Arbitrary FilePrefix where
    arbitrary = Test.QuickCheck.oneof [ pure Absolute, pure Here, pure Home ]

    shrink = genericShrink

instance Arbitrary Src where
    arbitrary = do
        lift2 Src <*> whitespace

    shrink (Src start end text) =
            (Src <$> shrink start <*> pure end   <*> pure text)
        ++  (Src <$> pure start   <*> shrink end <*> pure text)
        ++  (Src <$> pure start   <*> pure end   <*> shrinkWhitespace text)

instance Arbitrary SourcePos where
    arbitrary = lift3 SourcePos

    shrink = genericShrink

instance Arbitrary Pos where
    arbitrary = lift1 (Megaparsec.mkPos . getPositive)

instance Arbitrary ImportType where
    arbitrary =
        Test.QuickCheck.oneof
            [ do  prefix <- arbitrary

                  let nonEmptyText =
                          fmap Text.pack (Test.QuickCheck.listOf1 arbitrary)

                  components <- Test.QuickCheck.listOf nonEmptyText

                  file <- nonEmptyText

                  let directory = Directory{ components }

                  let path = File{ file, directory }

                  return (Local prefix path)
            , lift1 Remote
            , lift1 Env
            , lift0 Missing
            ]

    shrink = genericShrink

instance Arbitrary ImportHashed where
    arbitrary =
        lift1 (ImportHashed Nothing)

    shrink (ImportHashed { importType = oldImportType, .. }) = do
        newImportType <- shrink oldImportType
        let importHashed = ImportHashed { importType = newImportType, .. }
        return importHashed

-- The standard does not yet specify how to encode `as Text`, so don't test it
-- yet
instance Arbitrary ImportMode where
    arbitrary = Test.QuickCheck.elements [ Code, RawText, Location, RawBytes ]

    shrink = genericShrink

instance Arbitrary Import where
    arbitrary = lift2 Import

    shrink = genericShrink

instance Arbitrary Scheme where
    arbitrary = Test.QuickCheck.oneof [ pure HTTP, pure HTTPS ]

    shrink = genericShrink

instance Arbitrary URL where
    arbitrary = do
        scheme <- arbitrary

        -- TODO: the authority generator could be more precise, but it currently
        -- seems good enough.
        let validAuthorityChar =
                arbitrary `suchThat` \ch ->
                    not (Data.Char.isSpace ch) && not (Data.Char.isPunctuation ch)

        authority <- Text.pack <$> Test.QuickCheck.listOf validAuthorityChar

        let validPChar =
                Test.QuickCheck.frequency
                    [ (26, chooseCharacter ('A', 'Z'))
                    , (26, chooseCharacter ('a', 'z'))
                    , (10, chooseCharacter ('0', '9'))
                    , (17, Test.QuickCheck.elements "-._~!$&'*+;=:@")
                    ]

        let component = fmap Text.pack (Test.QuickCheck.listOf validPChar)

        components <- Test.QuickCheck.listOf component

        file <- component

        let directory = Directory{ components }

        let path = File{ file, directory }

        let validQueryCharacters =
                Test.QuickCheck.frequency
                    [ (79, validPChar)
                    , ( 2, Test.QuickCheck.elements "/?")
                    ]

        query <- Test.QuickCheck.oneof
            [ pure Nothing
            , fmap (Just . Text.pack) (Test.QuickCheck.listOf validQueryCharacters)
            ]

        headers <- arbitrary

        return URL{..}

    shrink _ = []

instance Arbitrary Var where
    arbitrary =
        Test.QuickCheck.oneof
            [ fmap (V "_") (getNonNegative <$> arbitrary)
            , fmap (\t -> V t 0) label
            , V <$> label <*> (getNonNegative <$> arbitrary)
            ]
    shrink = genericShrink

label :: Gen Text
label = fmap Text.pack (Test.QuickCheck.listOf labelCharacter)
  where
    labelCharacter =
        Test.QuickCheck.frequency
            [ (64, chooseCharacter ('\x20', '\x5F'))
            , (30, chooseCharacter ('\x61', '\x7e'))
            ]

binaryRoundtrip :: Expr () Import -> Property
binaryRoundtrip expression =
        Dhall.Binary.decodeExpression (Dhall.Binary.encodeExpression denotedExpression)
    === Right denotedExpression
  where
    denotedExpression :: Expr Void Import
    denotedExpression = denote' expression

    denote' :: Expr a Import -> Expr b Import
    denote' = Dhall.Core.denote . fmap denoteHttpHeaders

    denoteHttpHeaders import_@(Import importHashed _)
        | Remote url <- importType importHashed
        = let headers' = denote' <$> headers url
              importType' = Remote url { headers = headers' }
              importHashed' = importHashed { importType = importType' }
          in  import_ {importHashed = importHashed'}
        | otherwise = import_

everythingWellTypedNormalizes :: Expr () () -> Property
everythingWellTypedNormalizes expression =
        isRight (Dhall.TypeCheck.typeWithA filterOutEmbeds Dhall.Context.empty expression)
    ==> Test.QuickCheck.total (Dhall.Core.normalize expression :: Expr () ())
  where
    filterOutEmbeds :: Typer a
    filterOutEmbeds _ = Const Sort -- This could be any ill-typed expression.

isNormalizedIsConsistentWithNormalize :: Expr () Import -> Property
isNormalizedIsConsistentWithNormalize expression =
    case maybeProp of
        Nothing -> Test.QuickCheck.discard
        Just v -> v
  where
      denotedExpression :: Expr Void Import
      denotedExpression = Dhall.Core.denote expression

      maybeProp = do
          nf <- Control.Spoon.spoon (Dhall.Core.normalize expression)
          isNormalized <- Control.Spoon.spoon (Dhall.Core.isNormalized expression)
          -- Dhall.Core.isNormalized ignores 'Note's and other annotations.
          -- So we do the same when checking the result of 'normalize'.
          return $ isNormalized === (nf == denotedExpression)

normalizeWithMIsConsistentWithNormalize :: Expr () Import -> Property
normalizeWithMIsConsistentWithNormalize expression =
    case Control.Spoon.spoon (nfM, nf) of
        Just (a, b) -> a === b
        Nothing -> Test.QuickCheck.discard
  where nfM = runIdentity (Dhall.Core.normalizeWithM (\_ -> Identity Nothing) expression)
        nf = Dhall.Core.normalize expression :: Expr () Import

isSameAsSelf :: Expr () Import -> Property
isSameAsSelf expression =
  hasNoImportAndTypechecks ==> Dhall.Diff.same (Dhall.Diff.diff denoted denoted)
  where denoted = Dhall.Core.denote expression
        hasNoImportAndTypechecks =
          case traverse (\_ -> Left ()) expression of
            Right importlessExpression -> isRight (Dhall.TypeCheck.typeOf importlessExpression)
            Left _ -> False

inferredTypesAreNormalized :: Expr () Import -> Property
inferredTypesAreNormalized expression =
    Test.Tasty.QuickCheck.counterexample report (all Dhall.Core.isNormalized result)
  where
    report =  "Got: " ++ show result
           ++ "\nExpected: " ++ show (fmap Dhall.Core.normalize result
                                      :: Either (TypeError () Import) (Expr () Import))

    result = Dhall.TypeCheck.typeWithA filterOutEmbeds Dhall.Context.empty expression

    filterOutEmbeds :: Typer a
    filterOutEmbeds _ = Const Sort -- This could be any ill-typed expression.

normalizingAnExpressionDoesntChangeItsInferredType :: Expr () Import -> Property
normalizingAnExpressionDoesntChangeItsInferredType expression =
    case (eT0, eT1) of
        (Right t0, Right t1) -> t0 === t1
        _ -> Test.QuickCheck.discard
  where
    eT0 = typeCheck expression
    eT1 = typeCheck (Dhall.Core.normalize expression)

    typeCheck = Dhall.TypeCheck.typeWithA filterOutEmbeds Dhall.Context.empty

    filterOutEmbeds :: Typer a
    filterOutEmbeds _ = Const Sort -- This could be any ill-typed expression.

noDoubleNotes :: Expr () Import -> Property
noDoubleNotes expression =
    length
        [ ()
        | e <- Foldable.toList parsedExpression
        , Note _ (Note _ _) <- Lens.toListOf Dhall.Core.subExpressions e
        ] === 0
  where
    text = Dhall.Core.pretty expression

    parsedExpression = Parser.exprFromText "" text

embedThenExtractIsIdentity
    :: forall a. (ToDhall a, FromDhall a, Eq a, Typeable a, Arbitrary a, Show a)
    => Proxy a
    -> (String, Property, TestTree -> TestTree)
embedThenExtractIsIdentity p =
    ( "Embedding then extracting is identity for " ++ show (typeRep p)
    , Test.QuickCheck.property (prop :: a -> Bool)
    , adjustQuickCheckTests 1000
    )
  where
    prop a = case extract auto (embed inject a) of
        Success a' -> a == a'
        Failure _  -> False

idempotenceTest :: CharacterSet -> Header -> Expr Src Import -> Property
idempotenceTest characterSet header expr =
        not (any hasHttpHeaders expr)
    ==> let once = format characterSet (header, expr)
        in case Parser.exprAndHeaderFromText mempty once of
            Right (format characterSet -> twice) -> once === twice
            Left _ -> Test.QuickCheck.discard
  where
    -- Workaround for https://github.com/dhall-lang/dhall-haskell/issues/1925.
    hasHttpHeaders = \case
        Import (ImportHashed _ (Remote (URL { headers = Just _ }))) _ -> True
        _                                                             -> False

tests :: TestTree
tests =
    testProperties'
        "QuickCheck"
        [ ( "Binary serialization should round-trip"
          , Test.QuickCheck.property binaryRoundtrip
          , adjustQuickCheckTests 100
          )
        , ( "everything well-typed should normalize"
          , Test.QuickCheck.property everythingWellTypedNormalizes
          , adjustQuickCheckTests 100000
          )
        , ( "isNormalized should be consistent with normalize"
          , Test.QuickCheck.property isNormalizedIsConsistentWithNormalize
          , adjustQuickCheckTests 10000
          )
        , ( "normalizeWithM should be consistent with normalize"
          , Test.QuickCheck.property normalizeWithMIsConsistentWithNormalize
          , adjustQuickCheckTests 10000
          )
        , ( "An expression should have no difference with itself"
          , Test.QuickCheck.property isSameAsSelf
          , adjustQuickCheckTests 10000
          )
        , ( "Inferred types should be normalized"
          , Test.QuickCheck.property inferredTypesAreNormalized
          , adjustQuickCheckTests 10000
          )
        , ( "Normalizing an expression doesn't change its inferred type"
          , Test.QuickCheck.property normalizingAnExpressionDoesntChangeItsInferredType
          , adjustQuickCheckTests 10000
          )
        , ( "Parsing an expression doesn't generated doubly-nested Note constructors"
          , Test.QuickCheck.property noDoubleNotes
          , adjustQuickCheckTests 100
          )
        , embedThenExtractIsIdentity (Proxy :: Proxy (Text))
        , embedThenExtractIsIdentity (Proxy :: Proxy [Nat.Natural])
        , embedThenExtractIsIdentity (Proxy :: Proxy (Bool, Double))
        , embedThenExtractIsIdentity (Proxy :: Proxy (Data.Sequence.Seq ()))
        , embedThenExtractIsIdentity (Proxy :: Proxy (Maybe Integer))
        , embedThenExtractIsIdentity (Proxy :: Proxy (Data.Set.Set Nat.Natural))
        , embedThenExtractIsIdentity (Proxy :: Proxy (Data.HashSet.HashSet Text))
        , embedThenExtractIsIdentity (Proxy :: Proxy (Vector Double))
        , embedThenExtractIsIdentity (Proxy :: Proxy (Data.Map.Map Double Bool))
        , embedThenExtractIsIdentity (Proxy :: Proxy (HashMap.HashMap Double Bool))
        , ( "Formatting should be idempotent"
          , Test.QuickCheck.property idempotenceTest
          , adjustQuickCheckTests 10000
          )
        ]

adjustQuickCheckMaxRatio :: Int -> TestTree -> TestTree
adjustQuickCheckMaxRatio maxSize =
    Test.Tasty.adjustOption (max $ Test.Tasty.QuickCheck.QuickCheckMaxRatio maxSize)

adjustQuickCheckTests :: Int -> TestTree -> TestTree
adjustQuickCheckTests nTests =
    -- Using adjustOption instead of withMaxSuccess allows us to override the number of tests
    -- with the --quickcheck-tests CLI option.
    Test.Tasty.adjustOption (max $ QuickCheckTests nTests)

testProperties' :: String -> [(String, Property, TestTree -> TestTree)] -> TestTree
testProperties' name = Test.Tasty.testGroup name . map f
  where
    f (n, p, adjust) = adjust (Test.Tasty.QuickCheck.testProperty n p)