8000 crucible: Standalone kind signatures · Issue #1329 · GaloisInc/crucible · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

crucible: Standalone kind signatures #1329

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.

Sign up for GitHub

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

Jump to bottom
Open
langston-barrett opened this issue Mar 20, 2025 · 3 comments
Open

crucible: Standalone kind signatures #1329

langston-barrett opened this issue Mar 20, 2025 · 3 comments
Assignees
@langston-barrett
Labels
crucible documentation

Comments

@langston-barrett
Copy link
Contributor

Crucible has many datatypes and classes that have many type variables. These variables are infrequently documented, and there is a wide variety in when their kinds are provided in a kind signature. When they are, these kind signatures are generally inline, rather than standalone. Furthermore, I suspect that some of these type variables may be too polymorphic, as they occur in modules with PolyKinds, which will allow GHC to infer polymorphic kinds when possible.

For a demonstration of all of the above issues, consider the ExecutionTree module:

rg '(^data|PolyKinds)' crucible/src/Lang/Crucible/Simulator/ExecutionTree.hs

30:{-# LANGUAGE PolyKinds #-}
178:data GlobalPair sym (v :: Type) =
225:data AbortedResult sym ext where
251:data SomeFrame (f :: fk -> argk -> Type) = forall l a . SomeFrame !(f l a)
292:data PartialResult sym ext (v :: Type)
321:data ResolvedCall p sym ext ret where
344:data ExecResult p sym ext (r :: Type)
398:data ExecState p sym ext (rtp :: Type)
540:data RunningStateInfo blocks args
557:data ResolvedJump sym blocks
567:data ControlResumption p sym ext rtp f where
606:data PausedFrame p sym ext rtp f
622:data VFFOtherPath p sym ext ret f args
655:data ValueFromFrame p sym ext (ret :: Type) (f :: Type)
718:data PendingPartialMerges =
743:data ValueFromValue p sym ext (ret :: Type) (top_return :: CrucibleType)
870:data ReturnHandler (ret :: CrucibleType) p sym ext root f args where
908:data ActiveTree p sym ext root (f :: Type) args
963:data Override p sym ext (args :: Ctx CrucibleType) ret
971:data FnState p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType)
990:data ExtensionImpl p sym ext
1024:data SimContext (personality :: Type) (sym :: Type) (ext :: Type)
1126:data SimState p sym ext rtp f (args :: Maybe (Ctx.Ctx CrucibleType))
1132:data SomeSimState p sym ext rtp =

Providing standalone kind signatures could solve all of these issues and many more besides, and be a significant boon to readability.

While adding such kind signatures, we should consider adding Haddocks that document the various type parameters, as can be seen on OverrideSim and ValueFromValue.

GHC 9.8 and above have a -Wmissing-poly-kind-signatures flag that could be helpful in tracking down especially high-priority instances.

Note that SAKS were added in GHC 8.10. This is outside of our support window, so shouldn't be a problem.
@langston-barrett langston-barrett self-assigned this Mar 20, 2025
@langston-barrett
Copy link
Contributor Author

Ah, one disadvantage: SAKS are not rendered by Haddock (that issue is on an archived repository, but AFAICT applies to at least Haddock 2.30), whereas inline kind signatures are rendered.

Perhaps we could even consider just explictly calling out the kinds of variables in their Haddocks...? It would be an unfortunate duplication, but this is an unfortunate limitation for Haddock...

@RyanGlScott
Copy link
Contributor

Personally, I'd argue that the benefits of adding standalone kind signatures would outweigh their drawbacks.

It would also be nice to fix haskell/haddock#1178, of course. I have been meaning to look into this myself, but I haven't found the time to do so. This would be a fun project for someone who is looking to get involved with Haddock development—I'm happy to advise to the extent that I can.

@langston-barrett
Copy link
Contributor Author

Personally, I'd argue that the benefits of adding standalone kind signatures would outweigh their drawbacks.

I agree, so let's go for it.

This was referenced Mar 21, 2025
Merged
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@langston-barrett langston-barrett

Labels
crucible documentation
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@RyanGlScott @langston-barrett
0