Add the primitive equality type to Clash.Core.TysPrim
#1955
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Moving these types out of Clash.Core.Type means there is no longer a circular import between Clash.Core.TysPrim and Clash.Core.Type. This means we can access the whole of Clash.Core.Type without needing to expose anything more in .hs-boot files. We need this because the equality primitive type constructor (~#) has a polymoprhic type which we need to manually reconstruct in the TysPrim module, and currently cannot because not enough things are available when importing boot modules.
christiaanb
reviewed
Oct 13, 2021
christiaanb
approved these changes
Oct 13, 2021
The primitive type equality type is the basis of all typical type equality types you see in GHC (~ and ~~ are special within GHC but defined as though they are subclasses of a ~# b). As such this is the equality that often appears in GHC / Clash core when coercions are used in code (e.g. GADT pattern matches).
alex-mckenna
force-pushed
the
tysprim-equality
branch
from
7940f85
to
020022e
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds the primitive equality type (
~#) to the map of primitive type constructors that Clash knows about. The main motivation for adding this is the ability to generate arbitrary GADTs inclash-hedgehog, although it may also be useful in tidying up code inclash-libthat handles type equality (as a lot of~in user code become~#in GHC core).Still TODO: