purescript · TheMatten · May 29, 2021 · May 29, 2021 · May 31, 2021
diff --git 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/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
@@ -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

diff --git 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 (const 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