@@ -1,6 +1,8 @@
1−-- |
2−-- Subsumption checking
3−--
1+{-# LANGUAGE DataKinds #-}
2+{-# LANGUAGE GADTs #-}
3+{-# LANGUAGE TypeFamilies #-}
4+
5+-- | Subsumption checking
46module Language.PureScript.TypeChecker.Subsumption
57 ( subsumes
68 ) where
@@ -25,72 +27,120 @@ import Language.PureScript.TypeChecker.Skolems
2527import Language.PureScript.TypeChecker.Unify
2628import Language.PureScript.Types
2729
30+-- | Subsumption can operate in two modes:
31+--
32+-- * Elaboration mode, in which we try to insert type class dictionaries
33+-- * No-elaboration mode, in which we do not insert dictionaries
34+--
35+-- Some subsumption rules apply in both modes, and others are specific to
36+-- certain modes.
37+--
38+-- The subsumption algorithm follows the structure of the types in question,
39+-- and we can switch into no-elaboration mode when we move under a type
40+-- constructor where we can no longer insert dictionaries, e.g. into the fields
41+-- of a record.
42+data Mode = Elaborate | NoElaborate
43+
44+-- | Value-level proxies for the two modes
45+data ModeSing (mode :: Mode) where
46+ SElaborate :: ModeSing 'Elaborate
47+ SNoElaborate :: ModeSing 'NoElaborate
48+
49+-- | This type family tracks what evidence we return from 'subsumes' for each
50+-- mode.
51+type family Coercion (mode :: Mode) where
52+ -- When elaborating, we generate a coercion
53+ Coercion 'Elaborate = Expr -> Expr
54+ -- When we're not elaborating, we don't generate coercions
55+ Coercion 'NoElaborate = ()
56+
57+-- | The default coercion for each mode.
58+defaultCoercion :: ModeSing mode -> Coercion mode
59+defaultCoercion SElaborate = id
60+defaultCoercion SNoElaborate = ()
61+
2862-- | Check that one type subsumes another, rethrowing errors to provide a better error message
29−subsumes :: (MonadError MultipleErrors m, MonadState CheckState m) => Maybe Expr -> Type -> Type -> m (Maybe Expr)
30−subsumes val ty1 ty2 = withErrorMessageHint (ErrorInSubsumption ty1 ty2) $ subsumes' val ty1 ty2
63+subsumes
64+ :: (MonadError MultipleErrors m, MonadState CheckState m)
65+ => Type
66+ -> Type
67+ -> m (Expr -> Expr)
68+subsumes ty1 ty2 =
69+ withErrorMessageHint (ErrorInSubsumption ty1 ty2) $
70+ subsumes' SElaborate ty1 ty2
3171
3272-- | Check that one type subsumes another
33−subsumes' :: (MonadError MultipleErrors m, MonadState CheckState m) =>
34− Maybe Expr ->
35− Type ->
36− Type ->
37− m (Maybe Expr)
38−subsumes' val (ForAll ident ty1 _) ty2 = do
73+subsumes'
74+ :: (MonadError MultipleErrors m, MonadState CheckState m)
75+ => ModeSing mode
76+ -> Type
77+ -> Type
78+ -> m (Coercion mode)
79+subsumes' mode (ForAll ident ty1 _) ty2 = do
3980 replaced <- replaceVarWithUnknown ident ty1
40− subsumes val replaced ty2
41−subsumes' val ty1 (ForAll ident ty2 sco) =
81+ subsumes' mode replaced ty2
82+subsumes' mode ty1 (ForAll ident ty2 sco) =
4283 case sco of
4384 Just sco' -> do
4485 sko <- newSkolemConstant
4586 let sk = skolemize ident sko sco' Nothing ty2
46− subsumes val ty1 sk
87+ subsumes' mode ty1 sk
4788 Nothing -> internalError "subsumes: unspecified skolem scope"
48−subsumes' val (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do
49− _ <- subsumes Nothing arg2 arg1
50− _ <- subsumes Nothing ret1 ret2
51− return val
52−subsumes' val (KindedType ty1 _) ty2 =
53− subsumes val ty1 ty2
54−subsumes' val ty1 (KindedType ty2 _) =
55− subsumes val ty1 ty2
56−subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do
89+subsumes' mode (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do
90+ subsumes' SNoElaborate arg2 arg1
91+ subsumes' SNoElaborate ret1 ret2
92+ -- Nothing was elaborated, return the default coercion
93+ return (defaultCoercion mode)
94+subsumes' mode (KindedType ty1 _) ty2 =
95+ subsumes' mode ty1 ty2
96+subsumes' mode ty1 (KindedType ty2 _) =
97+ subsumes' mode ty1 ty2
98+-- Only check subsumption for constrained types when elaborating.
99+-- Otherwise fall back to unification.
100+subsumes' SElaborate (ConstrainedType constraints ty1) ty2 = do
57101 dicts <- getTypeClassDictionaries
58102 hints <- gets checkHints
59− subsumes' (Just $ foldl App val (map (\cs -> TypeClassDictionary cs dicts hints) constraints)) ty1 ty2
60−subsumes' val (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyRecord && f2 == tyRecord = do
61− let
62− (ts1, r1') = rowToList r1
63− (ts2, r2') = rowToList r2
64− ts1' = sortBy (comparing fst) ts1
65− ts2' = sortBy (comparing fst) ts2
66− -- For { ts1 | r1 } to subsume { ts2 | r2 } when r1 is empty (= we're working with a closed row),
67− -- every property in ts2 must appear in ts1. If not, then the candidate expression is missing a required property.
68− -- Conversely, when r2 is empty, every property in ts1 must appear in ts2, or else the expression has
69− -- an additional property which is not allowed.
70− when (r1' == REmpty)
71− (for_ (firstMissingProp ts2' ts1') (throwError . errorMessage . PropertyIsMissing . fst))
72− when (r2' == REmpty)
73− (for_ (firstMissingProp ts1' ts2') (throwError . errorMessage . AdditionalProperty . fst))
74− go ts1' ts2' r1' r2'
75− return val
103+ elaborate <- subsumes' SElaborate ty1 ty2
104+ let addDicts val = foldl App val (map (\cs -> TypeClassDictionary cs dicts hints) constraints)
105+ return (elaborate . addDicts)
106+subsumes' mode (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyRecord && f2 == tyRecord = do
107+ let
108+ (ts1, r1') = rowToList r1
109+ (ts2, r2') = rowToList r2
110+ ts1' = sortBy (comparing fst) ts1
111+ ts2' = sortBy (comparing fst) ts2
112+ -- For { ts1 | r1 } to subsume { ts2 | r2 } when r1 is empty (= we're working with a closed row),
113+ -- every property in ts2 must appear in ts1. If not, then the candidate expression is missing a required property.
114+ -- Conversely, when r2 is empty, every property in ts1 must appear in ts2, or else the expression has
115+ -- an additional property which is not allowed.
116+ when (r1' == REmpty)
117+ (for_ (firstMissingProp ts2' ts1') (throwError . errorMessage . PropertyIsMissing . fst))
118+ when (r2' == REmpty)
119+ (for_ (firstMissingProp ts1' ts2') (throwError . errorMessage . AdditionalProperty . fst))
120+ go ts1' ts2' r1' r2'
121+ -- Nothing was elaborated, return the default coercion
122+ return (defaultCoercion mode)
76123 where
77− go [] ts2 r1' r2' = unifyTypes r1' (rowFromList (ts2, r2'))
78− go ts1 [] r1' r2' = unifyTypes r2' (rowFromList (ts1, r1'))
79− go ((p1, ty1) : ts1) ((p2, ty2) : ts2) r1' r2'
80− | p1 == p2 = do _ <- subsumes Nothing ty1 ty2
81− go ts1 ts2 r1' r2'
82− | p1 < p2 = do rest <- freshType
83− -- What happens next is a bit of a hack.
84− -- TODO: in the new type checker, object properties will probably be restricted to being monotypes
85− -- in which case, this branch of the subsumes function should not even be necessary.
86− unifyTypes r2' (RCons p1 ty1 rest)
87− go ts1 ((p2, ty2) : ts2) r1' rest
88− | otherwise = do rest <- freshType
89− unifyTypes r1' (RCons p2 ty2 rest)
90− go ((p1, ty1) : ts1) ts2 rest r2'
91− -- Find the first property that's in the first list (of tuples) but not in the second
92− firstMissingProp t1 t2 = fst <$> uncons (minusBy' (comparing fst) t1 t2)
93−subsumes' val ty1 ty2@(TypeApp obj _) | obj == tyRecord = subsumes val ty2 ty1
94−subsumes' val ty1 ty2 = do
124+ go [] ts2 r1' r2' = unifyTypes r1' (rowFromList (ts2, r2'))
125+ go ts1 [] r1' r2' = unifyTypes r2' (rowFromList (ts1, r1'))
126+ go ((p1, ty1) : ts1) ((p2, ty2) : ts2) r1' r2'
127+ | p1 == p2 = do subsumes' SNoElaborate ty1 ty2
128+ go ts1 ts2 r1' r2'
129+ | p1 < p2 = do rest <- freshType
130+ -- What happens next is a bit of a hack.
131+ -- TODO: in the new type checker, object properties will probably be restricted to being monotypes
132+ -- in which case, this branch of the subsumes function should not even be necessary.
133+ unifyTypes r2' (RCons p1 ty1 rest)
134+ go ts1 ((p2, ty2) : ts2) r1' rest
135+ | otherwise = do rest <- freshType
136+ unifyTypes r1' (RCons p2 ty2 rest)
137+ go ((p1, ty1) : ts1) ts2 rest r2'
138+
139+ -- Find the first property that's in the first list (of tuples) but not in the second
140+ firstMissingProp t1 t2 = fst <$> uncons (minusBy' (comparing fst) t1 t2)
141+subsumes' mode ty1 ty2@(TypeApp obj _) | obj == tyRecord =
142+ subsumes' mode ty2 ty1
143+subsumes' mode ty1 ty2 = do
95144 unifyTypes ty1 ty2
96− return val
145+ -- Nothing was elaborated, return the default coercion
146+ return (defaultCoercion mode)