From 1e470e0be0522683978bb5b67a909a31bbcc1d0b Mon Sep 17 00:00:00 2001 From: TheMatten Date: Sat, 29 May 2021 14:33:46 +0200 Subject: [PATCH 1/3] Implement Typeable --- src/Language/PureScript/Constants/Prelude.hs | 11 +++++ .../PureScript/TypeChecker/Entailment.hs | 43 ++++++++++++++++++- 2 files changed, 52 insertions(+), 2 deletions(-) diff --git a/src/Language/PureScript/Constants/Prelude.hs b/src/Language/PureScript/Constants/Prelude.hs index 4a294256fc..25d6ddd665 100644 --- a/src/Language/PureScript/Constants/Prelude.hs +++ b/src/Language/PureScript/Constants/Prelude.hs @@ -376,6 +376,17 @@ pattern DataSymbol = ModuleName "Data.Symbol" pattern IsSymbol :: Qualified (ProperName 'ClassName) pattern IsSymbol = Qualified (Just DataSymbol) (ProperName "IsSymbol") +-- Type.Rep + +pattern TypeRep :: ModuleName +pattern TypeRep = ModuleName "Type.Rep" + +pattern Typeable :: Qualified (ProperName 'ClassName) +pattern Typeable = Qualified (Just TypeRep) (ProperName "Typeable") + +typeRep :: forall a. (IsString a) => a +typeRep = "typeRep" + prelude :: forall a. (IsString a) => a prelude = "Prelude" diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs index 5cf3419a9a..2b48cbcaa2 100644 --- a/src/Language/PureScript/TypeChecker/Entailment.hs +++ b/src/Language/PureScript/TypeChecker/Entailment.hs @@ -21,14 +21,16 @@ import Control.Monad.Writer import Data.Foldable (for_, fold, toList) import Data.Function (on) import Data.Functor (($>)) -import Data.List (findIndices, minimumBy, groupBy, nubBy, sortOn) +import Data.List (findIndices, foldl', minimumBy, groupBy, nubBy, sortOn) import Data.Maybe (fromMaybe, listToMaybe, mapMaybe) import qualified Data.Map as M import qualified Data.Set as S +import Data.String (fromString) import Data.Traversable (for) import Data.Text (Text, stripPrefix, stripSuffix) import qualified Data.Text as T import qualified Data.List.NonEmpty as NEL +import GHC.Fingerprint (Fingerprint, fingerprintString) import Language.PureScript.AST import Language.PureScript.Crash @@ -42,7 +44,7 @@ import Language.PureScript.TypeChecker.Unify import Language.PureScript.TypeClassDictionaries import Language.PureScript.Types import Language.PureScript.Label (Label(..)) -import Language.PureScript.PSString (PSString, mkString, decodeString) +import Language.PureScript.PSString (PSString, mkString, decodeString, decodeStringEither) import qualified Language.PureScript.Constants.Prelude as C import qualified Language.PureScript.Constants.Prim as C @@ -54,6 +56,7 @@ data Evidence -- | Computed instances | WarnInstance SourceType -- ^ Warn type class with a user-defined warning message | IsSymbolInstance PSString -- ^ The IsSymbol type class for a given Symbol literal + | TypeableInstance Fingerprint -- ^ The Typeable type class for a given type | EmptyClassInstance -- ^ For any solved type class with no members deriving (Show, Eq) @@ -176,6 +179,7 @@ entails SolverOptions{..} constraint context hints = -- This allows us to defer a warning by propagating the constraint. findDicts ctx cn Nothing ++ [TypeClassDictionaryInScope Nothing 0 (WarnInstance msg) [] C.Warn [] [] [msg] Nothing] forClassName _ _ C.IsSymbol _ args | Just dicts <- solveIsSymbol args = dicts + forClassName _ _ C.Typeable kinds args | Just dicts <- solveTypeable kinds args = dicts forClassName _ _ C.SymbolCompare _ args | Just dicts <- solveSymbolCompare args = dicts forClassName _ _ C.SymbolAppend _ args | Just dicts <- solveSymbolAppend args = dicts forClassName _ _ C.SymbolCons _ args | Just dicts <- solveSymbolCons args = dicts @@ -379,6 +383,9 @@ entails SolverOptions{..} constraint context hints = mkDictionary (IsSymbolInstance sym) _ = let fields = [ ("reflectSymbol", Abs (VarBinder nullSourceSpan UnusedIdent) (Literal nullSourceSpan (StringLiteral sym))) ] in return $ TypeClassDictionaryConstructorApp C.IsSymbol (Literal nullSourceSpan (ObjectLiteral fields)) + mkDictionary (TypeableInstance fp) _ = + let fields = [ (C.typeRep, Literal nullSourceSpan $ StringLiteral $ fromString $ show fp) ] in + return $ TypeClassDictionaryConstructorApp C.Typeable (Literal nullSourceSpan (ObjectLiteral fields)) unknownsInAllCoveringSets :: [SourceType] -> S.Set (S.Set Int) -> Bool unknownsInAllCoveringSets tyArgs = all (\s -> any (`S.member` s) unkIndices) @@ -416,6 +423,38 @@ entails SolverOptions{..} constraint context hints = solveIsSymbol [TypeLevelString ann sym] = Just [TypeClassDictionaryInScope Nothing 0 (IsSymbolInstance sym) [] C.IsSymbol [] [] [TypeLevelString ann sym] Nothing] solveIsSymbol _ = Nothing + solveTypeable :: [SourceType] -> [SourceType] -> Maybe [TypeClassDict] + solveTypeable [kind] [type_] + | Just tS <- normalizedTypeS type_ = Just + [TypeClassDictionaryInScope Nothing 0 (TypeableInstance $ fingerprintString $ tS "") [] C.Typeable [] [kind] [type_] Nothing] + where + normalizedTypeS t = case rowToSortedList t of + ([], t') -> case t' of + TypeLevelString _ s -> Just $ shows s + TypeConstructor _ (Qualified mn (ProperName cn)) -> Just $ + maybe id ((. showString ".") . showString . T.unpack . runModuleName) mn . showString (T.unpack cn) + TypeApp _ t1 t2 -> do + t1S <- normalizedTypeS t1 + t2S <- normalizedTypeS t2 + Just $ showString "(" . t1S . showString ")(" . t2S . showString ")" + KindApp _ t1 t2 -> do + t1S <- normalizedTypeS t1 + t2S <- normalizedTypeS t2 + Just $ showString "(" . t1S . showString ")@(" . t2S . showString ")" + REmpty _ -> Just $ showString "()" + _ -> Nothing + (row, isREmpty -> True) -> do + rowS <- normalizedRowS row + Just $ showString "(" . rowS . showString ")" + _ -> Nothing + normalizedRowS = foldl' go (Just id) where + go s (RowListItem _ (Label n) t) = do + s' <- s + lbl <- traverse (either (\_ -> Nothing) Just) $ decodeStringEither n + tS <- normalizedTypeS t + Just $ s' . showString lbl . showString "::" . tS . showString "," + solveTypeable _ _ = Nothing + solveSymbolCompare :: [SourceType] -> Maybe [TypeClassDict] solveSymbolCompare [arg0@(TypeLevelString _ lhs), arg1@(TypeLevelString _ rhs), _] = let ordering = case compare lhs rhs of From 7f3f9f0bbd6d5c390a28d9dc1eb7367038da2efd Mon Sep 17 00:00:00 2001 From: TheMatten Date: Sat, 29 May 2021 20:26:40 +0200 Subject: [PATCH 2/3] Apply hlint suggestions --- src/Language/PureScript/TypeChecker/Entailment.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs index 2b48cbcaa2..9460b75b1a 100644 --- a/src/Language/PureScript/TypeChecker/Entailment.hs +++ b/src/Language/PureScript/TypeChecker/Entailment.hs @@ -450,7 +450,7 @@ entails SolverOptions{..} constraint context hints = normalizedRowS = foldl' go (Just id) where go s (RowListItem _ (Label n) t) = do s' <- s - lbl <- traverse (either (\_ -> Nothing) Just) $ decodeStringEither n + lbl <- traverse (either (const Nothing) Just) $ decodeStringEither n tS <- normalizedTypeS t Just $ s' . showString lbl . showString "::" . tS . showString "," solveTypeable _ _ = Nothing From c2ec32b1176faf92e9091e87c70bab53681d8960 Mon Sep 17 00:00:00 2001 From: TheMatten Date: Mon, 31 May 2021 12:14:43 +0200 Subject: [PATCH 3/3] Disallow Typeable instance declarations --- src/Language/PureScript/Errors.hs | 10 +++++----- src/Language/PureScript/Sugar/TypeClasses.hs | 5 +++-- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/Language/PureScript/Errors.hs b/src/Language/PureScript/Errors.hs index 6fce239501..5a5cfd3aa0 100644 --- a/src/Language/PureScript/Errors.hs +++ b/src/Language/PureScript/Errors.hs @@ -183,7 +183,7 @@ data SimpleErrorMessage Text -- ^ Type variable in question Role -- ^ inferred role Role -- ^ declared role - | InvalidCoercibleInstanceDeclaration [SourceType] + | DisallowedInstanceDeclaration (Qualified (ProperName 'ClassName)) [SourceType] | UnsupportedRoleDeclaration | RoleDeclarationArityMismatch (ProperName 'TypeName) Int Int | DuplicateRoleDeclaration (ProperName 'TypeName) @@ -347,7 +347,7 @@ errorCode em = case unwrapErrorMessage em of VisibleQuantificationCheckFailureInType {} -> "VisibleQuantificationCheckFailureInType" UnsupportedTypeInKind {} -> "UnsupportedTypeInKind" RoleMismatch {} -> "RoleMismatch" - InvalidCoercibleInstanceDeclaration {} -> "InvalidCoercibleInstanceDeclaration" + DisallowedInstanceDeclaration {} -> "DisallowedInstanceDeclaration" UnsupportedRoleDeclaration {} -> "UnsupportedRoleDeclaration" RoleDeclarationArityMismatch {} -> "RoleDeclarationArityMismatch" DuplicateRoleDeclaration {} -> "DuplicateRoleDeclaration" @@ -467,7 +467,7 @@ onTypesInErrorMessageM f (ErrorMessage hints simple) = ErrorMessage <$> traverse gSimple (MissingTypeDeclaration nm ty) = MissingTypeDeclaration nm <$> f ty gSimple (MissingKindDeclaration sig nm ty) = MissingKindDeclaration sig nm <$> f ty gSimple (CannotGeneralizeRecursiveFunction nm ty) = CannotGeneralizeRecursiveFunction nm <$> f ty - gSimple (InvalidCoercibleInstanceDeclaration tys) = InvalidCoercibleInstanceDeclaration <$> traverse f tys + gSimple (DisallowedInstanceDeclaration cn tys) = DisallowedInstanceDeclaration cn <$> traverse f tys gSimple other = pure other gHint (ErrorInSubsumption t1 t2) = ErrorInSubsumption <$> f t1 <*> f t2 @@ -1319,11 +1319,11 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath) e = fl " is required." ] - renderSimpleErrorMessage (InvalidCoercibleInstanceDeclaration tys) = + renderSimpleErrorMessage (DisallowedInstanceDeclaration cn tys) = paras [ line "Invalid type class instance declaration for" , markCodeBox $ indent $ Box.hsep 1 Box.left - [ line (showQualified runProperName C.Coercible) + [ line (showQualified runProperName cn) , Box.vcat Box.left (map prettyTypeAtom tys) ] , line "Instance declarations of this type class are disallowed." diff --git a/src/Language/PureScript/Sugar/TypeClasses.hs b/src/Language/PureScript/Sugar/TypeClasses.hs index dcbb3472b4..15e97f9a3b 100644 --- a/src/Language/PureScript/Sugar/TypeClasses.hs +++ b/src/Language/PureScript/Sugar/TypeClasses.hs @@ -23,6 +23,7 @@ import qualified Data.Set as S import Data.Text (Text) import Data.Traversable (for) import qualified Language.PureScript.Constants.Prim as C +import qualified Language.PureScript.Constants.Prelude as C import Language.PureScript.Crash import Language.PureScript.Environment import Language.PureScript.Errors hiding (isExported) @@ -216,8 +217,8 @@ desugarDecl syns kinds mn exps = go go (TypeInstanceDeclaration _ _ _ _ _ _ _ DerivedInstance) = internalError "Derived instanced should have been desugared" go (TypeInstanceDeclaration _ _ _ (Left _) _ _ _ _) = internalError "instance names should have been desugared" go d@(TypeInstanceDeclaration sa _ _ (Right name) deps className tys (ExplicitInstance members)) - | className == C.Coercible - = throwError . errorMessage' (fst sa) $ InvalidCoercibleInstanceDeclaration tys + | className `elem` [C.Coercible, C.Typeable] + = throwError . errorMessage' (fst sa) $ DisallowedInstanceDeclaration className tys | otherwise = do desugared <- desugarCases members dictDecl <- typeInstanceDictionaryDeclaration syns kinds sa name mn deps className tys desugared