Skip to content

Commit d6d3943

Browse files
sjakobimergify[bot]
sjakobi
authored and
mergify[bot]
committed
Update type-inference of annotated expressions (dhall-lang#1337)
… as standardized in dhall-lang/dhall-lang#745. This also adds proper error handling for the free variable case discussed in dhall-lang/dhall-lang#749: Sample output for the MergeHandlerFreeVar test case: Error: Disallowed handler type Explanation: You can ❰merge❱ the alternatives of a union using a record with one handler per alternative, like this: ┌─────────────────────────────────────────────────────────────────┐ │ let union = < Left : Natural | Right : Bool >.Left 2 │ │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ │ in merge handlers union : Bool │ └─────────────────────────────────────────────────────────────────┘ ... but the output type of a handler may not depend on the input value. For example, the following expression is not valid: Invalid: The output type is ❰Optional A❱, which references the input value ❰A❱. ⇩ ┌──────────────────────────────────────────┐ │ merge { x = None } (< x : Type >.x Bool) │ └──────────────────────────────────────────┘ Your handler for the following alternative: ↳ x ... has type: ↳ ∀(A : Type) → Optional A ... where the output type: ↳ Optional A ... references the handler's input value: ↳ A ──────────────────────────────────────────────────────────────────────────────── 1│ merge { x = None } (<x: Type>.x Bool) dhall/dhall-lang/tests/type-inference/failure/unit/MergeHandlerFreeVar.dhall:1:1
1 parent 5595801 commit d6d3943

File tree

4 files changed

+163
-63
lines changed

4 files changed

+163
-63
lines changed

‎dhall/dhall-lang

Submodule dhall-lang updated 25 files

‎dhall/src/Dhall/Eval.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -975,7 +975,7 @@ quote !env !t0 =
975975
VConst k ->
976976
Const k
977977
VVar !x !i ->
978-
Var (V x (fromIntegral (countNames x env - i - 1)))
978+
Var (V x (countNames x env - i - 1))
979979
VApp t u ->
980980
quote env t `qApp` u
981981
VLam a (freshClosure -> (x, v, t)) ->

‎dhall/src/Dhall/TypeCheck.hs

Lines changed: 125 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,7 @@ import qualified Data.Set
5353
import qualified Data.Text as Text
5454
import qualified Data.Text.Prettyprint.Doc as Pretty
5555
import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty
56+
import qualified Data.Traversable
5657
import qualified Dhall.Context
5758
import qualified Dhall.Core
5859
import qualified Dhall.Diff
@@ -61,6 +62,7 @@ import qualified Dhall.Map
6162
import qualified Dhall.Set
6263
import qualified Dhall.Pretty.Internal
6364
import qualified Dhall.Util
65+
import qualified Lens.Family
6466

6567
type X = Void
6668

@@ -305,7 +307,7 @@ infer typer = loop
305307

306308
if Eval.conv values _T₀' _T₁'
307309
then do
308-
return _T₀'
310+
return _T₁'
309311

310312
else do
311313
let _T₀'' = quote names _T₀'
@@ -937,86 +939,100 @@ infer typer = loop
937939
then return ()
938940
else die (UnusedHandler diffT)
939941

940-
(my₀, _T₁') <- do
941-
case mT₁ of
942-
Just _T₁ -> do
943-
return (Nothing, eval values _T₁)
942+
if Data.Set.null diffU
943+
then return ()
944+
else die (MissingHandler diffU)
944945

945-
Nothing -> do
946-
case Dhall.Map.uncons yTs' of
947-
Nothing -> do
948-
die MissingMergeType
946+
let match _y _T₀' Nothing =
947+
return _T₀'
949948

950-
Just (y₀, _T', _) -> do
951-
_T₁' <- do
952-
case Dhall.Map.lookup y₀ yUs' of
953-
Nothing -> do
954-
die (UnusedHandler diffU)
949+
match y handler' (Just _A₁') =
950+
case Eval.toVHPi handler' of
951+
Just (x, _A₀', _T₀') -> do
952+
if Eval.conv values _A₀' _A₁'
953+
then do
954+
let _T₁' = _T₀' (fresh ctx x)
955955

956-
Just Nothing -> do
957-
return _T'
956+
let _T₁'' = quote names _T₁'
958957

959-
Just (Just _) -> do
960-
case Eval.toVHPi _T' of
961-
Just (x, _A₀', _T₀') -> do
962-
return (_T₀' (fresh ctx x))
958+
-- x appearing in _T₁'' would indicate a disallowed
959+
-- handler type (see
960+
-- https://github.com/dhall-lang/dhall-lang/issues/749).
961+
--
962+
-- If x appears in _T₁'', quote will have given it index
963+
-- -1. Any well-typed variable has a non-negative index,
964+
-- so we can simply look for negative indices to detect x.
965+
let containsBadVar (Var (V _ n)) =
966+
n < 0
963967

964-
Nothing -> do
965-
let _T'' = quote names _T'
968+
containsBadVar e =
969+
Lens.Family.anyOf
970+
Dhall.Core.subExpressions
971+
containsBadVar
972+
e
966973

967-
die (HandlerNotAFunction y₀ _T'')
974+
if containsBadVar _T₁''
975+
then do
976+
let handler'' = quote names handler'
968977

969-
return (Just y₀, _T₁')
978+
let outputType = Dhall.Core.shift 1 (V x (-1)) _T₁''
970979

971-
let _T₁'' = quote names _T₁'
980+
die (DisallowedHandlerType y handler'' outputType x)
972981

973-
_ <- loop ctx _T₁''
982+
else return _T₁'
974983

975-
let process y mU = do
976-
case Dhall.Map.lookup y yTs' of
977-
Nothing -> do
978-
die (MissingHandler diffU)
984+
else do
985+
let _A₀'' = quote names _A₀'
986+
let _A₁'' = quote names _A₁'
979987

980-
Just _T' -> do
981-
_T₃' <- do
982-
case mU of
983-
Nothing -> do
984-
return _T'
988+
die (HandlerInputTypeMismatch y _A₁'' _A₀'')
985989

986-
Just _A₁' -> do
987-
case Eval.toVHPi _T' of
988-
Just (x, _A₀', _T₂') -> do
989-
if Eval.conv values _A₀' _A₁'
990-
then do
991-
return ()
990+
Nothing -> do
991+
let handler'' = quote names handler'
992992

993-
else do
994-
let _A₀'' = quote names _A₀'
995-
let _A₁'' = quote names _A₁'
993+
die (HandlerNotAFunction y handler'')
996994

997-
die (HandlerInputTypeMismatch y _A₁'' _A₀'')
995+
matched <-
996+
sequence
997+
(Data.Map.intersectionWithKey match (Dhall.Map.toMap yTs') (Dhall.Map.toMap yUs'))
998998

999-
return (_T₂' (fresh ctx x))
999+
let checkMatched :: Data.Map.Map Text (Val a) -> Either (TypeError s a) (Maybe (Val a))
1000+
checkMatched = fmap (fmap snd) . Data.Foldable.foldlM go Nothing . Data.Map.toList
1001+
where
1002+
go Nothing (y₁, _T₁') =
1003+
return (Just (y₁, _T₁'))
10001004

1001-
Nothing -> do
1002-
let _T'' = quote names _T'
1005+
go yT₀'@(Just (y₀, _T₀')) (y₁, _T₁') =
1006+
if Eval.conv values _T₀' _T₁'
1007+
then return yT₀'
10031008

1004-
die (HandlerNotAFunction y _T'')
1009+
else do
1010+
let _T₀'' = quote names _T₀'
1011+
let _T₁'' = quote names _T₁'
1012+
die (HandlerOutputTypeMismatch y₀ _T₀'' y₁ _T₁'')
10051013

1006-
if Eval.conv values _T₁' _T₃'
1007-
then do
1008-
return ()
1014+
mT₀' <- checkMatched matched
10091015

1010-
else do
1011-
let _T₃'' = quote names _T₃'
1016+
mT₁' <- Data.Traversable.for mT₁ $ \_T₁ -> do
1017+
_ <- loop ctx _T₁
10121018

1013-
case my₀ of
1014-
Nothing -> die (InvalidHandlerOutputType y _T₁'' _T₃'')
1015-
Just y₀ -> die (HandlerOutputTypeMismatch y₀ _T₁'' y _T₃'')
1019+
return (eval values _T₁)
10161020

1017-
Dhall.Map.unorderedTraverseWithKey_ process yUs'
1021+
case (mT₀', mT₁') of
1022+
(Nothing, Nothing) ->
1023+
die MissingMergeType
1024+
(Nothing, Just _T₁') ->
1025+
return _T₁'
1026+
(Just _T₀', Nothing) ->
1027+
return _T₀'
1028+
(Just _T₀', Just _T₁') -> do
1029+
if Eval.conv values _T₀' _T₁'
1030+
then return _T₀'
10181031

1019-
return _T₁'
1032+
else do
1033+
let _T₀'' = quote names _T₀'
1034+
let _T₁'' = quote names _T₁'
1035+
die (AnnotMismatch (Merge t u Nothing) _T₁'' _T₀'')
10201036

10211037
ToMap e mT₁ -> do
10221038
_E' <- loop ctx e
@@ -1080,7 +1096,7 @@ infer typer = loop
10801096
die (InvalidToMapType _T₁'')
10811097
(Just (Right _T'), Just _T₁')
10821098
| Eval.conv values (mapType _T') _T₁' -> do
1083-
pure _T₁'
1099+
pure (mapType _T')
10841100
| otherwise -> do
10851101
let _T₁'' = quote names _T₁'
10861102

@@ -1292,6 +1308,7 @@ data TypeMessage s a
12921308
| UnusedHandler (Set Text)
12931309
| MissingHandler (Set Text)
12941310
| HandlerInputTypeMismatch Text (Expr s a) (Expr s a)
1311+
| DisallowedHandlerType Text (Expr s a) (Expr s a) Text
12951312
| HandlerOutputTypeMismatch Text (Expr s a) Text (Expr s a)
12961313
| InvalidHandlerOutputType Text (Expr s a) (Expr s a)
12971314
| MissingMergeType
@@ -3140,6 +3157,52 @@ prettyTypeMessage (HandlerInputTypeMismatch expr0 expr1 expr2) =
31403157
txt1 = insert expr1
31413158
txt2 = insert expr2
31423159

3160+
prettyTypeMessage (DisallowedHandlerType label handlerType handlerOutputType variable) =
3161+
ErrorMessages {..}
3162+
where
3163+
short = "Disallowed handler type"
3164+
3165+
long =
3166+
"Explanation: You can ❰merge❱ the alternatives of a union using a record with one\n\
3167+
\handler per alternative, like this: \n\
3168+
\ \n\
3169+
\ \n\
3170+
\ ┌─────────────────────────────────────────────────────────────────┐ \n\
3171+
\ │ let union = < Left : Natural | Right : Bool >.Left 2 │ \n\
3172+
\ │ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
3173+
\ │ in merge handlers union : Bool │ \n\
3174+
\ └─────────────────────────────────────────────────────────────────┘ \n\
3175+
\ \n\
3176+
\ \n\
3177+
\... but the output type of a handler may not depend on the input value. \n\
3178+
\ \n\
3179+
\For example, the following expression is " <> _NOT <> " valid: \n\
3180+
\ \n\
3181+
\ \n\
3182+
\ Invalid: The output type is ❰Optional A❱, which references the input \n\
3183+
\ value ❰A❱. \n\
3184+
\ ⇩ \n\
3185+
\ ┌──────────────────────────────────────────┐ \n\
3186+
\ │ merge { x = None } (< x : Type >.x Bool) │ \n\
3187+
\ └──────────────────────────────────────────┘ \n\
3188+
\ \n\
3189+
\ \n\
3190+
\Your handler for the following alternative: \n\
3191+
\ \n\
3192+
\" <> insert label <> "\n\
3193+
\ \n\
3194+
\... has type: \n\
3195+
\ \n\
3196+
\" <> insert handlerType <> "\n\
3197+
\ \n\
3198+
\... where the output type: \n\
3199+
\ \n\
3200+
\" <> insert handlerOutputType <> "\n\
3201+
\ \n\
3202+
\... references the handler's input value: \n\
3203+
\ \n\
3204+
\" <> insert variable <> "\n"
3205+
31433206
prettyTypeMessage (InvalidHandlerOutputType expr0 expr1 expr2) =
31443207
ErrorMessages {..}
31453208
where
@@ -4295,6 +4358,8 @@ messageExpressions f m = case m of
42954358
MissingHandler <$> pure a
42964359
HandlerInputTypeMismatch a b c ->
42974360
HandlerInputTypeMismatch <$> pure a <*> f b <*> f c
4361+
DisallowedHandlerType a b c d ->
4362+
DisallowedHandlerType <$> pure a <*> f b <*> f c <*> pure d
42984363
HandlerOutputTypeMismatch a b c d ->
42994364
HandlerOutputTypeMismatch <$> pure a <*> f b <*> pure c <*> f d
43004365
InvalidHandlerOutputType a b c ->

‎dhall/tests/Dhall/Test/QuickCheck.hs

Lines changed: 36 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ import Dhall.Core
3232
import Data.Functor.Identity (Identity(..))
3333
import Dhall.Set (Set)
3434
import Dhall.Src (Src(..))
35-
import Dhall.TypeCheck (Typer)
35+
import Dhall.TypeCheck (Typer, TypeError)
3636
import Generic.Random (Weights, W, (%), (:+)(..))
3737
import Test.QuickCheck
3838
(Arbitrary(..), Gen, Positive(..), Property, NonNegative(..), genericShrink, (===), (==>))
@@ -405,6 +405,33 @@ isSameAsSelf expression =
405405
Right importlessExpression -> isRight (Dhall.TypeCheck.typeOf importlessExpression)
406406
Left _ -> False
407407

408+
inferredTypesAreNormalized :: Expr () Import -> Property
409+
inferredTypesAreNormalized expression =
410+
Test.Tasty.QuickCheck.counterexample report (all Dhall.Core.isNormalized result)
411+
where
412+
report = "Got: " ++ show result
413+
++ "\nExpected: " ++ show (fmap Dhall.Core.normalize result
414+
:: Either (TypeError () Import) (Expr () Import))
415+
416+
result = Dhall.TypeCheck.typeWithA filterOutEmbeds Dhall.Context.empty expression
417+
418+
filterOutEmbeds :: Typer a
419+
filterOutEmbeds _ = Const Sort -- This could be any ill-typed expression.
420+
421+
normalizingAnExpressionDoesntChangeItsInferredType :: Expr () Import -> Property
422+
normalizingAnExpressionDoesntChangeItsInferredType expression =
423+
case (eT0, eT1) of
424+
(Right t0, Right t1) -> t0 === t1
425+
_ -> Test.QuickCheck.discard
426+
where
427+
eT0 = typeCheck expression
428+
eT1 = typeCheck (Dhall.Core.normalize expression)
429+
430+
typeCheck = Dhall.TypeCheck.typeWithA filterOutEmbeds Dhall.Context.empty
431+
432+
filterOutEmbeds :: Typer a
433+
filterOutEmbeds _ = Const Sort -- This could be any ill-typed expression.
434+
408435
tests :: TestTree
409436
tests =
410437
testProperties'
@@ -429,6 +456,14 @@ tests =
429456
, Test.QuickCheck.property isSameAsSelf
430457
, QuickCheckTests 10000
431458
)
459+
, ( "Inferred types should be normalized"
460+
, Test.QuickCheck.property inferredTypesAreNormalized
461+
, QuickCheckTests 10000
462+
)
463+
, ( "Normalizing an expression doesn't change its inferred type"
464+
, Test.QuickCheck.property normalizingAnExpressionDoesntChangeItsInferredType
465+
, QuickCheckTests 10000
466+
)
432467
]
433468

434469
testProperties' :: String -> [(String, Property, QuickCheckTests)] -> TestTree

0 commit comments

Comments
 (0)