dhall-golang icon indicating copy to clipboard operation
dhall-golang copied to clipboard

alphaEquivalence tries to compare (potentially) incomparable values

Open Trundle opened this issue 4 years ago • 0 comments

A minimal example I could come up with was assert : List/head {} ≡ List/head {}, which panics dhall-golang:

panic: runtime error: comparing uncomparable type core.RecordType

goroutine 1 [running]:
github.com/philandstuff/dhall-golang/v6/core.alphaEquivalentWith(0x0, 0x9504e0, 0xc0005513e0, 0x9504e0, 0xc0005513f0, 0x950780)
	/tmp/dhall-golang/core/equivalence.go:29 +0x372
github.com/philandstuff/dhall-golang/v6/core.AlphaEquivalent(...)
	/tmp/dhall-golang/core/equivalence.go:12
github.com/philandstuff/dhall-golang/v6/core.typeWith(0xc0003dfb90, 0x950900, 0xc000551320, 0x0, 0x0, 0x950900, 0xc000551320)
	/tmp/dhall-golang/core/typecheck.go:806 +0x18bb
github.com/philandstuff/dhall-golang/v6/core.TypeOf(...)
	/tmp/dhall-golang/core/typecheck.go:60
main.cmdDebug(0xc00054acc0, 0xc000549800, 0x1)
	/tmp/dhall-golang/cmd/main.go:51 +0x157
github.com/urfave/cli/v2.(*App).RunContext(0xc000001980, 0x958220, 0xc000024270, 0xc0000201e0, 0x1, 0x1, 0x0, 0x0)
	/home/andy/go/pkg/mod/github.com/urfave/cli/[email protected]/app.go:315 +0x70d
github.com/urfave/cli/v2.(*App).Run(...)
	/home/andy/go/pkg/mod/github.com/urfave/cli/[email protected]/app.go:215
main.main()
	/tmp/dhall-golang/cmd/main.go:35 +0x1b1
exit status 2

My analysis of what goes wrong (can be completely wrong): Certain built-ins store a Value in their struct to represent partial application, but Value isn't generally comparable using the equal operator. More specifically, RecordLit, RecordType and UnionType aren't comparable. And alphaEquivalence then doesn't take into account that (random example) a listHead is not comparable if it embeds a RecordType as typ field, as demonstrated in the initial example:

https://github.com/philandstuff/dhall-golang/blob/bcdfb6007e7007af7a24858d73baf0dc7538af46/core/equivalence.go#L17-L29

I think this can be solved by introducing more cases:

case listHead:
	v2, ok := v2.(listHead)
	return ok && alphaEquivalentWith(level, v1.typ, v2.typ)

I can come up with a pull request if that sounds like a suitable solution.

Trundle avatar Dec 23 '20 22:12 Trundle