Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

alphaEquivalence tries to compare (potentially) incomparable values #59

Open
Trundle opened this issue Dec 23, 2020 · 0 comments
Open

Comments

@Trundle
Copy link
Contributor

Trundle commented Dec 23, 2020

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:

case Universe, Builtin,
naturalBuild, naturalEven, naturalFold,
naturalIsZero, naturalOdd, naturalShow,
naturalSubtract, naturalToInteger,
integerShow, integerClamp, integerNegate, integerToDouble,
doubleShow,
optional, none,
textShow, textReplace,
list, listBuild, listFold, listHead, listIndexed,
listLength, listLast, listReverse,
freeVar, localVar, quoteVar,
NaturalLit, IntegerLit, BoolLit, PlainTextLit:
return v1 == v2

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant