search

matt-noonan / gdp

Ghosts of Departed Proofs
BSD 3-Clause "New" or "Revised" License
60 stars 11 forks source link

PolyKinded Equality #5

Closed shangaslammi closed 5 years ago

shangaslammi commented 5 years ago

Would it break anything to allow all kinds for the parameters of the Equality type? This would allow equality proofs that use promoted data types or e.g. Nats.

matt-noonan commented 5 years ago

I don't think there is any problem with this. Is it as simple as adding {-# LANGUAGE PolyKinds #-} in Theory.Equality, or are there other changes that would also be needed?