A variety of fixes to unification, substitution, and specialisation of GADTs - Githubissues

granule-project / granule

A statically-typed linear functional language with graded modal types for fine-grained program reasoning

https://granule-project.github.io

BSD 3-Clause "New" or "Revised" License

589 stars 33 forks source link

A variety of fixes to unification, substitution, and specialisation of GADTs #198

Closed dorchard closed 1 year ago

dorchard commented 1 year ago

A perennial problem within Granule v0.9 is around the interaction of substitution, unification, constraint solving (via the SMT) in the service of doing indexed types (GADTs). This branch is towards resolving this but is not yet done. For a while there has been some moving of the lump under the carpet between polymorphism and indexed types.

[ ] polymorphism tests all need to pass (i.e., stack test --test-arguments='-p polymorphism')
[ ] indexed tests all need to pass (i.e., stack test --test-arguments='-p indexed')

dorchard commented 1 year ago

Replaced with a different PR https://github.com/granule-project/granule/pull/208