Fixing the typechecking rule for Optional + with ?

[winitzki]

The corrected typechecking rules should be as follows:

Γ ⊢ e : Optional T₀
Γ ⊢ v : T₁
T₀ ≡ T₁
──────────────────────────────────
Γ ⊢ e with ? = v : Optional T₀


Γ ⊢ e : Optional T₀
Γ, x : T₀ ⊢ x with k.ks… = v : T₁
T₀ ≡ T₁
────────────────────────────────── x ∉ FV(v)
Γ ⊢ e with ?.k.ks… = v : Optional T₀

Two rules are necessary because we need to process e with ? = v and e with ?.x = v in different ways.

The types are now checked correctly:

⊢ (Some { a = 1 }) with ? = { a = 2 }

Some { a = 2 }

⊢ (Some { a = 1 }) with ?.a = { a = 2 }

Error: ❰with❱ cannot change the type of an ❰Optional❱ value

1│ (Some { a = 1 }) with ?.a = { a = 2 }

(input):1:1
⊢ (Some { a = 1 }) with ?.a = 2

Some { a = 2 }

⊢ (Some { a = 1 }) with ?.x.y = { a = 2 }

Error: ❰with❱ cannot change the type of an ❰Optional❱ value

1│ (Some { a = 1 }) with ?.x.y = { a = 2 }

(input):1:1
⊢ (Some { x = { y = 1 } }) with ?.x.y = 2

Some { x.y = 2 }

⊢ (Some { x = { y = 1 } }) with ?.x.y = "b"

Error: ❰with❱ cannot change the type of an ❰Optional❱ value

Could someone please help me with adding unit tests and with adding standard regression tests to dhall-lang/dhall-lang as well?

[winitzki]

How can I run the tests locally? I tried stack test but it failed with an error about gcc.

$ stack test
doctest         > configure
doctest         > Configuring doctest-0.22.6...
doctest         > build with ghc-9.6.6
doctest         > Preprocessing library for doctest-0.22.6..
doctest         > Building library for doctest-0.22.6..
doctest         > [ 1 of 25] Compiling Imports
doctest         > [ 2 of 25] Compiling GhcUtil
doctest         > [ 3 of 25] Compiling Cabal.Paths
doctest         > [ 4 of 25] Compiling Cabal.Options
doctest         > [ 5 of 25] Compiling Language.Haskell.GhciWrapper
doctest         > [ 6 of 25] Compiling Interpreter
doctest         > [ 7 of 25] Compiling Location
doctest         > [ 8 of 25] Compiling PackageDBs
doctest         > [ 9 of 25] Compiling Paths_doctest
doctest         > [10 of 25] Compiling Info
doctest         > [11 of 25] Compiling Options
doctest         > [12 of 25] Compiling Cabal
doctest         > [13 of 25] Compiling Test.DocTest.Internal.Cabal
doctest         > [14 of 25] Compiling Test.DocTest.Internal.Location
doctest         > [15 of 25] Compiling Util
doctest         > [16 of 25] Compiling Extract
doctest         > [17 of 25] Compiling Test.DocTest.Internal.Extract
doctest         > [18 of 25] Compiling Parse
doctest         > [19 of 25] Compiling Test.DocTest.Internal.Parse
doctest         > [20 of 25] Compiling Runner.Example
doctest         > [21 of 25] Compiling Property
doctest         > [22 of 25] Compiling Runner
doctest         > [23 of 25] Compiling Run
doctest         > [24 of 25] Compiling Test.DocTest.Internal.Run
doctest         > [25 of 25] Compiling Test.DocTest
doctest         > ld: warning: search path '/usr/local/lib' not found
doctest         > Preprocessing executable 'doctest' for doctest-0.22.6..
doctest         > Building executable 'doctest' for doctest-0.22.6..
doctest         > [1 of 2] Compiling Main
doctest         > [2 of 2] Compiling Paths_doctest
doctest         > [3 of 3] Linking .stack-work/dist/aarch64-osx/ghc-9.6.6/build/doctest/doctest
doctest         > ld: warning: ignoring duplicate library '-lm'
doctest         > ld: warning: search path '/usr/local/lib' not found
doctest         > ld: '_stg_upd_frame_info' from '/Users/user/.stack/programs/aarch64-osx/ghc-9.6.6/lib/ghc-9.6.6/lib/aarch64-osx-ghc-9.6.6/rts-1.0.2/libHSrts-1.0.2_thr.a[142](Updates.thr_o)' not 87-byte aligned, which cannot be encoded as a target of LDR/STR in '' from '/Users/user/.stack/programs/aarch64-osx/ghc-9.6.6/lib/ghc-9.6.6/lib/aarch64-osx-ghc-9.6.6/ghc-9.6.6/libHSghc-9.6.6.a[307](Instances.o)'
doctest         > clang: error: linker command failed with exit code 1 (use -v to see invocation)
doctest         > ghc-9.6.6: `gcc' failed in phase `Linker'. (Exit code: 1)
Progress 1/18

Error: [S-7282]
       Stack failed to execute the build plan.

       While executing the build plan, Stack encountered the error:

       [S-7011]
       While building package doctest-0.22.6 (scroll up to its section to see the error) using:
       /Users/user/.stack/setup-exe-cache/aarch64-osx/Cabal-simple_w2MFVN35_3.10.3.0_ghc-9.6.6 --verbose=1 --builddir=.stack-work/dist/aarch64-osx/ghc-9.6.6 build --ghc-options " -fdiagnostics-color=always"
       Process exited with code: ExitFailure 1

I have gcc installed:

$ gcc --version
Apple clang version 15.0.0 (clang-1500.0.38.1)
Target: arm64-apple-darwin22.6.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin

[winitzki]

I made a PR to add regression tests to dhall-lang here: dhall-lang/dhall-lang#1400

But I can't run tests locally. stack test fails with some error about gcc. I don't know even where to look to fix it.

Problems with GHC were fixed by upgrading my Mac. I will run tests locally when time permits.

[winitzki]

I ran locally the tests from the branch winitzki:feature/issue-2597-regression-with in dhall-lang, all tests passed.

[winitzki]

The test error is:

   Error: Server temporarily unavailable
        
        HTTP status code: 503
        
        URL: https://httpbin.org/user-agent

We should really stop using httpbin.org in tests. Instead, perhaps implement a barebones http server in bash / netcat or something like that.