Skip to content

Commit a465784

Browse files
kl0tlkl0tl
committed
Forbid heterogenously kinded Coercible constraints arguments
1 parent e4c5304 commit a465784

5 files changed

Lines changed: 90 additions & 42 deletions

File tree

‎lib/purescript-ast/src/Language/PureScript/Types.hs‎

Lines changed: 2 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,11 @@ import Codec.Serialise (Serialise)
1010
import Control.Applicative ((<|>))
1111
import Control.Arrow (first, second)
1212
import Control.DeepSeq (NFData)
13-
import Control.Monad ((<=<), (>=>), replicateM)
14-
import Control.Monad.Supply (runSupply)
15-
import Control.Monad.Supply.Class (fresh)
13+
import Control.Monad ((<=<), (>=>))
1614
import Data.Aeson ((.:), (.:?), (.!=), (.=))
1715
import qualified Data.Aeson as A
1816
import qualified Data.Aeson.Types as A
19-
import Data.Foldable (fold, foldl')
17+
import Data.Foldable (fold)
2018
import qualified Data.IntSet as IS
2119
import Data.List (sort, sortBy)
2220
import Data.Ord (comparing)
@@ -587,17 +585,6 @@ unapplyConstraints = go []
587585
go acc (ConstrainedType _ con ty) = go (con : acc) ty
588586
go acc ty = (reverse acc, ty)
589587

590-
saturate :: S.Set Text -> SourceType -> Int -> SourceType
591-
saturate bound ty n = fst . runSupply 0 $ do
592-
tvs <- replicateM n freshTyVar
593-
return $ foldl' srcTypeApp ty (srcTypeVar <$> tvs)
594-
where
595-
freshTyVar = do
596-
tv <- ("t" <>) . T.pack . show <$> fresh
597-
if tv `elem` bound
598-
then freshTyVar
599-
else return tv
600-
601588
everywhereOnTypes :: (Type a -> Type a) -> Type a -> Type a
602589
everywhereOnTypes f = go where
603590
go (TypeApp ann t1 t2) = f (TypeApp ann (go t1) (go t2))

‎src/Language/PureScript/TypeChecker/Entailment.hs‎

Lines changed: 37 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -14,14 +14,15 @@ module Language.PureScript.TypeChecker.Entailment
1414
import Prelude.Compat
1515
import Protolude (ordNub)
1616

17-
import Control.Applicative ((<|>))
17+
import Control.Applicative ((<|>), empty)
1818
import Control.Arrow (second, (&&&))
1919
import Control.Monad.Error.Class (MonadError(..))
2020
import Control.Monad.State
2121
import Control.Monad.Supply.Class (MonadSupply(..))
22+
import Control.Monad.Trans.Maybe (MaybeT(..))
2223
import Control.Monad.Writer
2324

24-
import Data.Foldable (for_, fold, toList)
25+
import Data.Foldable (for_, fold, foldl', toList)
2526
import Data.Function (on)
2627
import Data.Functor (($>))
2728
import Data.List (minimumBy, groupBy, nubBy, sortBy, zipWith4)
@@ -39,7 +40,7 @@ import Language.PureScript.Environment
3940
import Language.PureScript.Errors
4041
import Language.PureScript.Names
4142
import Language.PureScript.Roles
42-
import Language.PureScript.TypeChecker.Kinds (elaborateKind, unifyKinds)
43+
import Language.PureScript.TypeChecker.Kinds (elaborateKind, kindOf, unifyKinds)
4344
import Language.PureScript.TypeChecker.Monad
4445
import Language.PureScript.TypeChecker.Roles
4546
import Language.PureScript.TypeChecker.Synonyms
@@ -168,12 +169,18 @@ entails
168169
entails SolverOptions{..} constraint context hints =
169170
solve constraint
170171
where
172+
forClassNameM :: Environment -> InstanceContext -> Qualified (ProperName 'ClassName) -> [SourceType] -> [SourceType] -> m [TypeClassDict]
173+
forClassNameM env ctx cn@C.Coercible kinds args =
174+
solveCoercible env kinds args >>=
175+
pure . fromMaybe (forClassName env ctx cn kinds args)
176+
forClassNameM env ctx cn kinds args =
177+
pure $ forClassName env ctx cn kinds args
178+
171179
forClassName :: Environment -> InstanceContext -> Qualified (ProperName 'ClassName) -> [SourceType] -> [SourceType] -> [TypeClassDict]
172180
forClassName _ ctx cn@C.Warn _ [msg] =
173181
-- Prefer a warning dictionary in scope if there is one available.
174182
-- This allows us to defer a warning by propagating the constraint.
175183
findDicts ctx cn Nothing ++ [TypeClassDictionaryInScope [] 0 (WarnInstance msg) [] C.Warn [] [] [msg] Nothing]
176-
forClassName env _ C.Coercible kinds args | Just dicts <- solveCoercible env kinds args = dicts
177184
forClassName _ _ C.IsSymbol _ args | Just dicts <- solveIsSymbol args = dicts
178185
forClassName _ _ C.SymbolCompare _ args | Just dicts <- solveSymbolCompare args = dicts
179186
forClassName _ _ C.SymbolAppend _ args | Just dicts <- solveSymbolAppend args = dicts
@@ -225,10 +232,12 @@ entails SolverOptions{..} constraint context hints =
225232
Nothing -> throwError . errorMessage $ UnknownClass className'
226233
Just tcd -> pure tcd
227234

235+
dicts <- lift . lift $ forClassNameM env (combineContexts context inferred) className' kinds'' tys''
236+
228237
let instances = do
229238
chain <- groupBy ((==) `on` tcdChain) $
230239
sortBy (compare `on` (tcdChain &&& tcdIndex)) $
231-
forClassName env (combineContexts context inferred) className' kinds'' tys''
240+
dicts
232241
-- process instances in a chain in index order
233242
let found = for chain $ \tcd ->
234243
-- Make sure the type unifies with the type in the type instance definition
@@ -381,11 +390,11 @@ entails SolverOptions{..} constraint context hints =
381390
subclassDictionaryValue dict className index =
382391
App (Accessor (mkString (superclassName className index)) dict) valUndefined
383392

384-
solveCoercible :: Environment -> [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
385-
solveCoercible env kinds [a, b] = do
393+
solveCoercible :: Environment -> [SourceType] -> [SourceType] -> m (Maybe [TypeClassDict])
394+
solveCoercible env kinds [a, b] = runMaybeT $ do
386395
let tySynMap = typeSynonyms env
387396
kindMap = types env
388-
replaceTySyns = either (const Nothing) Just . replaceAllTypeSynonymsM tySynMap kindMap
397+
replaceTySyns = lift . replaceAllTypeSynonymsM tySynMap kindMap
389398
a' <- replaceTySyns a
390399
b' <- replaceTySyns b
391400
-- Solving terminates when the two arguments are the same. Since we
@@ -394,40 +403,43 @@ entails SolverOptions{..} constraint context hints =
394403
if a' == b'
395404
then pure [TypeClassDictionaryInScope [] 0 EmptyClassInstance [] C.Coercible [] kinds [a, b] Nothing]
396405
else do
406+
lift $ do
407+
(_, kind) <- kindOf a'
408+
(_, kind') <- kindOf b'
409+
unifyKinds kind kind'
397410
-- When solving must reduce and recurse, it doesn't matter whether we
398411
-- reduce the first or second argument -- if the constraint is
399412
-- solvable, either path will yield the same outcome. Consequently we
400413
-- just try the first argument first and the second argument second.
401-
ws <- coercibleWanteds env a' b' <|> coercibleWanteds env b' a'
414+
ws <- (MaybeT $ coercibleWanteds env a' b') <|> (MaybeT $ coercibleWanteds env b' a')
402415
pure [TypeClassDictionaryInScope [] 0 EmptyClassInstance [] C.Coercible [] kinds [a, b] (Just ws)]
403-
solveCoercible _ _ _ = Nothing
416+
solveCoercible _ _ _ = pure Nothing
404417

405418
-- | Take two types, @a@ and @b@ representing a desired constraint
406419
-- @Coercible a b@ and reduce them to a set of simpler wanted constraints
407420
-- whose satisfaction will yield the goal.
408-
coercibleWanteds :: Environment -> SourceType -> SourceType -> Maybe [SourceConstraint]
421+
coercibleWanteds :: Environment -> SourceType -> SourceType -> m (Maybe [SourceConstraint])
409422
coercibleWanteds env a b
410423
| (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
411424
, (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
412425
, Just (aTyKind, _) <- M.lookup aTyName $ types env
413426
, Just (bTyKind, _) <- M.lookup bTyName $ types env
414427
, (aks, kind) <- unapplyKinds aTyKind
415428
, (bks, _) <- unapplyKinds bTyKind
416-
, i <- length aks - length axs
417-
, j <- length bks - length bxs
418-
, i > 0 && j > 0 = do
429+
, length axs < length aks
430+
, length bxs < length bks = do
419431
-- If both arguments have kind @k1 -> k2@ (e.g. @data D a b = D a@
420432
-- in the constraint @Coercible (D a) (D a')@), yield a new wanted
421433
-- constraint in terms of the types saturated with the same variables
422434
-- (e.g. @Coercible (D a t0) (D a' t0)@ in the exemple).
423-
let aTyVars = S.fromList $ usedTypeVariables a
424-
bTyVars = S.fromList $ usedTypeVariables b
425-
saturate' = saturate $ aTyVars `S.union` bTyVars
426-
pure [srcCoercibleConstraint kind (saturate' a i) (saturate' b j)]
435+
tys <- traverse freshTypeWithKind aks
436+
let a' = foldl' srcTypeApp a $ drop (length axs) tys
437+
b' = foldl' srcTypeApp b $ drop (length bxs) tys
438+
pure $ Just [srcCoercibleConstraint kind a' b']
427439
| (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
428440
, (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
429441
, not (null axs) && not (null bxs) && aTyName == bTyName
430-
, Just (aTyKind, _) <- M.lookup aTyName (types env) = do
442+
, Just (aTyKind, _) <- M.lookup aTyName (types env) = runMaybeT $ do
431443
-- If both arguments are applications of the same type constructor
432444
-- (e.g. @data D a b = D a@ in the constraint
433445
-- @Coercible (D a b) (D a' b')@), infer the roles of the type
@@ -445,13 +457,13 @@ entails SolverOptions{..} constraint context hints =
445457
-- means there are cases we should be able to handle that
446458
-- we currently can't, but is at least sound.
447459
| ax == bx ->
448-
Just []
460+
pure []
449461
| otherwise ->
450-
Nothing
462+
empty
451463
Representational ->
452-
Just [srcCoercibleConstraint kx ax bx]
464+
pure [srcCoercibleConstraint kx ax bx]
453465
Phantom ->
454-
Just []
466+
pure []
455467
fmap concat $ sequence $ zipWith4 f roles kinds axs bxs
456468
| (TypeConstructor _ tyName, _, xs) <- unapplyTypes a
457469
, Just (tvs, wrappedTy, _) <- lookupNewtypeConstructor env tyName = do
@@ -461,10 +473,10 @@ entails SolverOptions{..} constraint context hints =
461473
-- terms of that type with the type arguments substituted in (e.g.
462474
-- @Coercible (T[X/a]) b = Coercible X b@ in the example).
463475
let wrappedTySub = replaceAllTypeVars (zip tvs xs) wrappedTy
464-
pure [srcCoercibleConstraint kindType wrappedTySub b]
476+
pure $ Just [srcCoercibleConstraint kindType wrappedTySub b]
465477
| otherwise =
466478
-- In all other cases we can't solve the constraint.
467-
Nothing
479+
pure Nothing
468480

469481
srcCoercibleConstraint :: SourceType -> SourceType -> SourceType -> SourceConstraint
470482
srcCoercibleConstraint k a b = srcConstraint C.Coercible [k] [a, b] Nothing

‎tests/purs/failing/CoercibleHigherKindedNewtypes.out‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,16 +4,20 @@ at tests/purs/failing/CoercibleHigherKindedNewtypes.purs:13:8 - 13:14 (line 13,
44

55
No type class instance was found for
66
 
7-
 Prim.Coerce.Coercible t1
8-
 t0
7+
 Prim.Coerce.Coercible t0
8+
 t1
99
 
10+
The instance head contains unknown type variables. Consider adding a type annotation.
1011

1112
while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
1213
is at least as general as type Ap @Type @Type N1 Int String -> Ap @Type @Type N2 Int String
1314
while checking that expression coerce
1415
has type Ap @Type @Type N1 Int String -> Ap @Type @Type N2 Int String
1516
in value declaration swap
1617

18+
where t1 is an unknown type
19+
t0 is an unknown type
20+
1721
See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
1822
or to contribute content related to this error.
1923

‎tests/purs/failing/CoercibleKindMismatch.out‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
Error found:
2+
in module Main
3+
at tests/purs/failing/CoercibleKindMismatch.purs:17:39 - 17:45 (line 17, column 39 - line 17, column 45)
4+
5+
Could not match kind
6+
 
7+
 Type
8+
 
9+
with kind
10+
 
11+
 Type -> Type
12+
 
13+
14+
while solving type class constraint
15+
 
16+
 Prim.Coerce.Coercible Unary 
17+
 Binary
18+
 
19+
while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
20+
is at least as general as type Proxy @(Type -> Type) Unary -> Proxy @(Type -> ...) Binary
21+
while checking that expression coerce
22+
has type Proxy @(Type -> Type) Unary -> Proxy @(Type -> ...) Binary
23+
in value declaration unaryToBinary
24+
25+
See https://github.com/purescript/documentation/blob/master/errors/KindsDoNotUnify.md for more information,
26+
or to contribute content related to this error.
27+

‎tests/purs/failing/CoercibleKindMismatch.purs‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
-- @shouldFailWith KindsDoNotUnify
2+
module Main where
3+
4+
import Safe.Coerce (coerce)
5+
6+
data Unary :: Type -> Type
7+
data Unary a
8+
9+
data Binary :: Type -> Type -> Type
10+
data Binary a b
11+
12+
data Proxy :: forall k. k -> Type
13+
data Proxy a = Proxy
14+
15+
type role Proxy representational
16+
17+
unaryToBinary :: Proxy Unary -> Proxy Binary
18+
unaryToBinary = coerce

0 commit comments

Comments
 (0)