@@ -1,6 +1,8 @@
1−-- |
1+{-# LANGUAGE DataKinds #-}
3+{-# LANGUAGE TypeFamilies #-}
2−-- Subsumption checking
5+-- | Subsumption checking
4module Language.PureScript.TypeChecker.Subsumption
6module Language.PureScript.TypeChecker.Subsumption
@@ -25,72 +27,120 @@ import Language.PureScript.TypeChecker.Skolems
25import Language.PureScript.TypeChecker.Unify
27import Language.PureScript.TypeChecker.Unify
26import Language.PureScript.Types
28import Language.PureScript.Types
30+-- | Subsumption can operate in two modes:
32+-- * Elaboration mode, in which we try to insert type class dictionaries
33+-- * No-elaboration mode, in which we do not insert dictionaries
35+-- Some subsumption rules apply in both modes, and others are specific to
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
42+data Mode = Elaborate | NoElaborate
44+-- | Value-level proxies for the two modes
45+data ModeSing (mode :: Mode) where
46+ SElaborate :: ModeSing 'Elaborate
47+ SNoElaborate :: ModeSing 'NoElaborate
49+-- | This type family tracks what evidence we return from 'subsumes' for each
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 = ()
57+-- | The default coercion for each mode.
58+defaultCoercion :: ModeSing mode -> Coercion mode
59+defaultCoercion SElaborate = id
60+defaultCoercion SNoElaborate = ()
28-- | Check that one type subsumes another, rethrowing errors to provide a better error message
62-- | 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)
64+ :: (MonadError MultipleErrors m, MonadState CheckState m)
30−subsumes val ty1 ty2 = withErrorMessageHint (ErrorInSubsumption ty1 ty2) $ subsumes' val ty1 ty2
69+ withErrorMessageHint (ErrorInSubsumption ty1 ty2) $
70+ subsumes' SElaborate ty1 ty2
32-- | Check that one type subsumes another
72-- | Check that one type subsumes another
33−subsumes' :: (MonadError MultipleErrors m, MonadState CheckState m) =>
74+ :: (MonadError MultipleErrors m, MonadState CheckState m)
34− Maybe Expr ->
75+ => ModeSing mode
37− m (Maybe Expr)
78+ -> m (Coercion mode)
38−subsumes' val (ForAll ident ty1 _) ty2 = do
79+subsumes' mode (ForAll ident ty1 _) ty2 = do
39 replaced <- replaceVarWithUnknown ident ty1
80 replaced <- replaceVarWithUnknown ident ty1
40− subsumes val replaced ty2
81+ subsumes' mode replaced ty2
41−subsumes' val ty1 (ForAll ident ty2 sco) =
82+subsumes' mode ty1 (ForAll ident ty2 sco) =
42 case sco of
83 case sco of
43 Just sco' -> do
84 Just sco' -> do
44 sko <- newSkolemConstant
85 sko <- newSkolemConstant
45 let sk = skolemize ident sko sco' Nothing ty2
86 let sk = skolemize ident sko sco' Nothing ty2
46− subsumes val ty1 sk
87+ subsumes' mode ty1 sk
47 Nothing -> internalError "subsumes: unspecified skolem scope"
88 Nothing -> internalError "subsumes: unspecified skolem scope"
48−subsumes' val (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do
89+subsumes' mode (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do
49− _ <- subsumes Nothing arg2 arg1
90+ subsumes' SNoElaborate arg2 arg1
50− _ <- subsumes Nothing ret1 ret2
91+ subsumes' SNoElaborate ret1 ret2
51− return val
92+ -- Nothing was elaborated, return the default coercion
93+ return (defaultCoercion mode)
52−subsumes' val (KindedType ty1 _) ty2 =
94+subsumes' mode (KindedType ty1 _) ty2 =
53− subsumes val ty1 ty2
95+ subsumes' mode ty1 ty2
54−subsumes' val ty1 (KindedType ty2 _) =
96+subsumes' mode ty1 (KindedType ty2 _) =
55− subsumes val ty1 ty2
97+ subsumes' mode ty1 ty2
98+-- Only check subsumption for constrained types when elaborating.
99+-- Otherwise fall back to unification.
56−subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do
100+subsumes' SElaborate (ConstrainedType constraints ty1) ty2 = do
57 dicts <- getTypeClassDictionaries
101 dicts <- getTypeClassDictionaries
58 hints <- gets checkHints
102 hints <- gets checkHints
103+ elaborate <- subsumes' SElaborate ty1 ty2
59− subsumes' (Just $ foldl App val (map (\cs -> TypeClassDictionary cs dicts hints) constraints)) ty1 ty2
104+ let addDicts val = foldl App val (map (\cs -> TypeClassDictionary cs dicts hints) constraints)
105+ return (elaborate . addDicts)
60−subsumes' val (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyRecord && f2 == tyRecord = do
106+subsumes' mode (TypeApp f1 r1) (TypeApp f2 r2) | f1 == tyRecord && f2 == tyRecord = do
62− (ts1, r1') = rowToList r1
108+ (ts1, r1') = rowToList r1
63− (ts2, r2') = rowToList r2
109+ (ts2, r2') = rowToList r2
64− ts1' = sortBy (comparing fst) ts1
110+ ts1' = sortBy (comparing fst) ts1
65− ts2' = sortBy (comparing fst) ts2
111+ ts2' = sortBy (comparing fst) ts2
66− -- For { ts1 | r1 } to subsume { ts2 | r2 } when r1 is empty (= we're working with a closed row),
112+ -- 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.
113+ -- 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
114+ -- 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.
115+ -- an additional property which is not allowed.
70− when (r1' == REmpty)
116+ when (r1' == REmpty)
71− (for_ (firstMissingProp ts2' ts1') (throwError . errorMessage . PropertyIsMissing . fst))
117+ (for_ (firstMissingProp ts2' ts1') (throwError . errorMessage . PropertyIsMissing . fst))
72− when (r2' == REmpty)
118+ when (r2' == REmpty)
73− (for_ (firstMissingProp ts1' ts2') (throwError . errorMessage . AdditionalProperty . fst))
119+ (for_ (firstMissingProp ts1' ts2') (throwError . errorMessage . AdditionalProperty . fst))
74− go ts1' ts2' r1' r2'
120+ go ts1' ts2' r1' r2'
75− return val
121+ -- Nothing was elaborated, return the default coercion
122+ return (defaultCoercion mode)
77− go [] ts2 r1' r2' = unifyTypes r1' (rowFromList (ts2, r2'))
124+ go [] ts2 r1' r2' = unifyTypes r1' (rowFromList (ts2, r2'))
78− go ts1 [] r1' r2' = unifyTypes r2' (rowFromList (ts1, r1'))
125+ go ts1 [] r1' r2' = unifyTypes r2' (rowFromList (ts1, r1'))
79− go ((p1, ty1) : ts1) ((p2, ty2) : ts2) r1' r2'
126+ go ((p1, ty1) : ts1) ((p2, ty2) : ts2) r1' r2'
80− | p1 == p2 = do _ <- subsumes Nothing ty1 ty2
127+ | p1 == p2 = do subsumes' SNoElaborate ty1 ty2
81− go ts1 ts2 r1' r2'
128+ go ts1 ts2 r1' r2'
82− | p1 < p2 = do rest <- freshType
129+ | p1 < p2 = do rest <- freshType
83− -- What happens next is a bit of a hack.
130+ -- 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
131+ -- 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.
132+ -- in which case, this branch of the subsumes function should not even be necessary.
86− unifyTypes r2' (RCons p1 ty1 rest)
133+ unifyTypes r2' (RCons p1 ty1 rest)
87− go ts1 ((p2, ty2) : ts2) r1' rest
134+ go ts1 ((p2, ty2) : ts2) r1' rest
88− | otherwise = do rest <- freshType
135+ | otherwise = do rest <- freshType
89− unifyTypes r1' (RCons p2 ty2 rest)
136+ unifyTypes r1' (RCons p2 ty2 rest)
90− go ((p1, ty1) : ts1) ts2 rest r2'
137+ 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
139+ -- 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)
140+ firstMissingProp t1 t2 = fst <$> uncons (minusBy' (comparing fst) t1 t2)
93−subsumes' val ty1 ty2@(TypeApp obj _) | obj == tyRecord = subsumes val ty2 ty1
141+subsumes' mode ty1 ty2@(TypeApp obj _) | obj == tyRecord =
142+ subsumes' mode ty2 ty1
94−subsumes' val ty1 ty2 = do
143+subsumes' mode ty1 ty2 = do
95 unifyTypes ty1 ty2
144 unifyTypes ty1 ty2
96− return val
145+ -- Nothing was elaborated, return the default coercion
146+ return (defaultCoercion mode)