Reject custom contexts that are ill-formed #259
Conversation
Fixes #253 This protects `typeWith` to reject any custom-context that might trigger a type-checking loop
src/Dhall/TypeCheck.hs
Outdated
| {-| This function verifies that a custom context is well-formed so that | ||
| type-checking will not loop | ||
| -} | ||
| checkContext :: Context (Expr s X) -> Either (TypeError s X) () |
There was a problem hiding this comment.
I think you meant to export this. If not, please export it 😄
There was a problem hiding this comment.
Actually, I intentionally did not export it since typeWith calls it once before entering the type-checking loop. This avoids the performance issue since it's not called on every iteration of the loop
|
Isn't it called twice though in the case where you are using the import
mechanism? It would still be nice to be able to do the check yourself.
…On Tue, 13 Feb 2018, 1:09 am Gabriel Gonzalez, ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In src/Dhall/TypeCheck.hs
<#259 (comment)>
:
> @@ -3254,3 +3256,18 @@ instance (Buildable a, Buildable s) => Buildable (DetailedTypeError s a) where
source = case expr of
Note s _ -> build s
_ -> mempty
+
+{-| This function verifies that a custom context is well-formed so that
+ type-checking will not loop
+-}
+checkContext :: Context (Expr s X) -> Either (TypeError s X) ()
Actually, I intentionally did not export it since typeWith calls it once
before entering the type-checking loop. This avoids the performance issue
since it's not called on every iteration of the loop
—
You are receiving this because your review was requested.
Reply to this email directly, view it on GitHub
<#259 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AABRjmy6HqzLSLlMjhUZHHhEbvWOoLe_ks5tUODXgaJpZM4SDEYB>
.
|
|
Oh, whoops! You're right that there is one unnecessary call to I'll also go ahead and export it, too |
|
Oh, I actually meant https://hackage.haskell.org/package/dhall-1.9.1/docs/src/Dhall-Import.html#loadWithContext which calls typeWith, so we end up validating the context twice if you do import resolution and then final type checking. It's hardly the end of the world though. |
|
Imports are type-checked twice anyway even without custom contexts. This is normal to ensure that imports are closed and also to localize error messages better. |
|
Sure, it's just a pinch more overhead. But I think it's inconsequential |
|
I'll go ahead and merge this, then, since I think I've addressed your requests |
Fixes #253
This protects
typeWithto reject any custom-context that might trigger atype-checking loop