Skip to content

Commit

Permalink
fixed bugs in backticked infix expressions & superclass variables types
Browse files Browse the repository at this point in the history
  • Loading branch information
gnumonik committed May 25, 2024
1 parent 426c4ff commit ff0b89f
Show file tree
Hide file tree
Showing 30 changed files with 311 additions and 570 deletions.
20 changes: 14 additions & 6 deletions src/Language/PureScript/CST/Convert.hs
Original file line number Diff line number Diff line change
Expand Up @@ -52,16 +52,24 @@ type ConvertM a = State (Map Text T.SourceType) a
runConvert :: ConvertM a -> a
runConvert ma = evalState ma M.empty

tvKind :: Text -> ConvertM T.SourceType
tvKind nm = do
tvKind :: SourceToken -> Text -> ConvertM T.SourceType
tvKind srcTok nm = do
cxt <- get
case M.lookup nm cxt of
Nothing -> internalError $ "Error: Missing kind annotation for TyVar " <> Text.unpack nm
Nothing -> internalError
$ "Error: Missing kind annotation for TyVar " <> Text.unpack nm
<> "\n at (or near): " <> prettyRange (srcTokenRange srcTok)
Just t -> pure t
where
prettyRange (SourceRange start end) = goPos start <> "-" <> goPos end
goPos (SourcePos line col) = show line <> ":" <> show col

bindTv :: Text -> T.SourceType -> ConvertM ()
bindTv nm ty = modify' (M.insert nm ty)

srcTokenRange :: SourceToken -> SourceRange
srcTokenRange = tokRange . tokAnn

{- Our new way of handling kinds introduces an annoying problem:
We need to have the kinds of tyvars bound the decl kind signature or
Expand Down Expand Up @@ -191,7 +199,7 @@ convertType' withinVta fileName = go
bindTv nm kd'
pure $ T.TypeVar (sourceName fileName a) (getIdent $ nameValue a) kd'
TypeVar _ a -> do
kd <- tvKind (getIdent $ nameValue a)
kd <- tvKind (nameTok a) (getIdent $ nameValue a)
pure $ T.TypeVar (sourceName fileName a) (getIdent $ nameValue a) kd
TypeConstructor _ a ->
pure $ T.TypeConstructor (sourceQualName fileName a) $ qualified a
Expand Down Expand Up @@ -412,7 +420,7 @@ convertExpr fileName = go
a' <- go a
b' <- go b
c' <- go c
pure $ positioned ann $ AST.BinaryNoParens a' b' c'
pure $ positioned ann $ AST.BinaryNoParens b' a' c'
expr@(ExprOp _ _ _ _) -> do
let
ann = uncurry (sourceAnn fileName) $ exprRange expr
Expand Down Expand Up @@ -769,7 +777,7 @@ convertDeclaration fileName decl = case decl of
pure (nm,k)
TypeVarName (_, x) -> do
let nm = getIdent (nameValue x)
ki <- tvKind nm
ki <- tvKind (nameTok x) nm
pure (nm,ki)

goInstanceBinding = \case
Expand Down
69 changes: 62 additions & 7 deletions src/Language/PureScript/TypeChecker/Kinds.hs
Original file line number Diff line number Diff line change
Expand Up @@ -58,16 +58,57 @@ import Language.PureScript.Types
import Language.PureScript.Pretty.Types (prettyPrintType)
import Language.PureScript.CST.Types (Comment)

import Data.Bifunctor (bimap)
import Debug.Trace
import Language.PureScript.CoreFn.Pretty.Types (prettyTypeStr)

moduleTraces :: Bool
moduleTraces = True

goTrace :: forall x. String -> x -> x
goTrace str x
| moduleTraces = trace str x
| otherwise = x

goTraceM :: forall f. Applicative f => String -> f ()
goTraceM msg
| moduleTraces = traceM msg
| otherwise = pure ()

spacer = '\n' : replicate 20 '-'
prettySubstitution :: Substitution -> String

prettySubstitution Substitution{..} =
"SUBSTITUTION: "
<> "\n SUBST_TYPE: " <> show (bimap show prettyTypeStr <$> M.toList substType)
<> "\n SUBST_UNSOLVED: " <> show (bimap show (bimap show prettyTypeStr) <$> M.toList substUnsolved)
<> "\n SUBST_NAMES: " <> show (M.toList substNames)

-- TODO/REVIEW/HACK: -----------------------------------
-- NO CLUE IF THE CHANGES I MADE HERE ARE CORRECT
generalizeUnknowns :: [(Unknown, SourceType)] -> SourceType -> SourceType
generalizeUnknowns unks ty =
generalizeUnknowns unks ty = goTrace msg $
generalizeUnknownsWithVars (unknownVarNames (fst <$> usedTypeVariables ty) unks) ty
where
result = generalizeUnknownsWithVars (unknownVarNames (fst <$> usedTypeVariables ty) unks) ty
msg = "GENERALIZE UNKNOWNS:\nUNKNOWNS" <> prettyUnknowns
<> "\n INPUT TYPE: " <> prettyTypeStr ty
<> "\n OUTPUT TYPE: " <> prettyTypeStr result
<> spacer
prettyUnknowns = concatMap (\x -> show (fst x) <> " :: " <> show (snd x) <> "\n") unks


generalizeUnknownsWithVars :: [(Unknown, (Text, SourceType))] -> SourceType -> SourceType
generalizeUnknownsWithVars binders ty =
generalizeUnknownsWithVars binders ty = goTrace msg $
mkForAll ((getAnnForType ty,) . fmap (replaceUnknownsWithVars binders) . snd <$> binders) . replaceUnknownsWithVars binders $ ty
where
prettyBinders :: [(Unknown, (Text, SourceType))] -> String
prettyBinders xs = concatMap (\x -> show (fst x) <> ", " <> T.unpack (fst (snd x)) <> " := " <> prettyTypeStr (snd (snd x)) <> "\n") xs

msg = "GENERALIZE UNKNOWNS WITH VARS:"
<> "\n UNKNOWNS: " <> prettyBinders binders
<> "\n TYPE: " <> prettyTypeStr ty
<> spacer

replaceUnknownsWithVars :: [(Unknown, (Text, SourceType))] -> SourceType -> SourceType
replaceUnknownsWithVars binders ty
Expand All @@ -92,7 +133,11 @@ unknownVarNames used unks =
vars = fmap (("k" <>) . T.pack . show) ([1..] :: [Int])

apply :: (MonadState CheckState m) => SourceType -> m SourceType
apply ty = flip substituteType ty <$> gets checkSubstitution
apply ty = goTrace msg $ flip substituteType ty <$> gets checkSubstitution
where
msg = "APPLY"
<> "\n TYPE: " <> prettyTypeStr ty
<> spacer

substituteType :: Substitution -> SourceType -> SourceType
substituteType sub = everywhereOnTypes $ \case
Expand Down Expand Up @@ -163,8 +208,13 @@ inferKind
-> m (SourceType, SourceType)
inferKind = \tyToInfer ->
withErrorMessageHint (ErrorInferringKind tyToInfer)
. rethrowWithPosition (fst $ getAnnForType tyToInfer)
$ go tyToInfer
. rethrowWithPosition (fst $ getAnnForType tyToInfer) $ do
result <- go tyToInfer
let msg = "\nINFERKIND INPUT: " <> prettyTypeStr tyToInfer
<> "\nINFERKIND RESULT: " <> prettyTypeStr (snd result)
<> "\n" <> replicate 20 '-'
goTraceM msg
pure result
where
go = \case
ty@(TypeConstructor ann v) -> do
Expand Down Expand Up @@ -339,7 +389,7 @@ instantiateKind
-> SourceType
-> m SourceType
instantiateKind (ty, kind1) kind2 = case kind1 of
ForAll _ _ a ( k) t _ | shouldInstantiate kind2 -> do
ForAll _ _ a k t _ | shouldInstantiate kind2 -> do
let ann = getAnnForType ty
u <- freshKindWithKind (fst ann) k
instantiateKind (KindApp ann ty u, replaceTypeVars a u t) kind2
Expand Down Expand Up @@ -423,7 +473,7 @@ unifyKindsWithFailure
unifyKindsWithFailure onFailure = go
where
goWithLabel l t1 t2 = withErrorMessageHint (ErrorInRowLabel l) $ go t1 t2
go = curry $ \case
go tx1 tx2 = goTrace msg $ case (tx1,tx2) of
(TypeApp _ p1 p2, TypeApp _ p3 p4) -> do
go p1 p3
join $ go <$> apply p2 <*> apply p4
Expand All @@ -446,6 +496,11 @@ unifyKindsWithFailure onFailure = go
solveUnknown a' p1
(w1, w2) ->
onFailure w1 w2
where
msg = "UNIFY KINDS WITH FAILURE"
<> "\n Ty1: " <> prettyTypeStr tx1
<> "\n Ty2: " <> prettyTypeStr tx2
<> "\n" <> replicate 20 '-'

unifyRows r1 r2 = do
let (matches, rest) = alignRowsWith goWithLabel r1 r2
Expand Down
26 changes: 24 additions & 2 deletions src/Language/PureScript/TypeChecker/Subsumption.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,25 @@ import Language.PureScript.TypeChecker.Skolems (newSkolemConstant, skolemize)
import Language.PureScript.TypeChecker.Unify (alignRowsWith, freshTypeWithKind, unifyTypes)
import Language.PureScript.Types (RowListItem(..), SourceType, Type(..), eqType, isREmpty, replaceTypeVars, rowFromList)

import Language.PureScript.CoreFn.Pretty.Types (prettyTypeStr)
import Debug.Trace ( trace, traceM )

moduleTraces :: Bool
moduleTraces = True

goTrace :: forall x. String -> x -> x
goTrace str x
| moduleTraces = trace str x
| otherwise = x

goTraceM :: forall f. Applicative f => String -> f ()
goTraceM msg
| moduleTraces = traceM msg
| otherwise = pure ()

spacer = "\n" <> replicate 20 '-'


-- | Subsumption can operate in two modes:
--
-- * Elaboration mode, in which we try to insert type class dictionaries
Expand Down Expand Up @@ -63,10 +82,13 @@ subsumes
=> SourceType
-> SourceType
-> m (Expr -> Expr)
subsumes ty1 ty2 =
subsumes ty1 ty2 = goTrace msg $
withErrorMessageHint (ErrorInSubsumption ty1 ty2) $
subsumes' SElaborate ty1 ty2

where
msg = "SUBSUMES"
<> "\n TYPE 1: " <> prettyTypeStr ty1
<> "\n TYPE 2: " <> prettyTypeStr ty2
-- | Check that one type subsumes another
subsumes'
:: (MonadError MultipleErrors m, MonadState CheckState m)
Expand Down
90 changes: 79 additions & 11 deletions src/Language/PureScript/TypeChecker/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -57,12 +57,13 @@ import Data.List.NonEmpty qualified as NEL
import Data.Map qualified as M
import Data.Set qualified as S
import Data.IntSet qualified as IS
import Data.Text qualified as T

import Language.PureScript.AST
import Language.PureScript.Crash (internalError)
import Language.PureScript.Environment
import Language.PureScript.Errors (ErrorMessage(..), MultipleErrors, SimpleErrorMessage(..), errorMessage, errorMessage', escalateWarningWhen, internalCompilerError, onErrorMessages, onTypesInErrorMessage, parU)
import Language.PureScript.Names (pattern ByNullSourcePos, Ident(..), ModuleName, Name(..), ProperName(..), ProperNameType(..), Qualified(..), QualifiedBy(..), byMaybeModuleName, coerceProperName, freshIdent)
import Language.PureScript.Names (pattern ByNullSourcePos, Ident(..), ModuleName, Name(..), ProperName(..), ProperNameType(..), Qualified(..), QualifiedBy(..), byMaybeModuleName, coerceProperName, freshIdent, runModuleName, runIdent)
import Language.PureScript.TypeChecker.Deriving (deriveInstance)
import Language.PureScript.TypeChecker.Entailment (InstanceContext, newDictionaries, replaceTypeClassDictionaries)
import Language.PureScript.TypeChecker.Kinds (checkConstraint, checkKind, checkTypeKind, kindOf, kindOfWithScopedVars, unifyKinds', unknownsWithKinds)
Expand All @@ -76,6 +77,27 @@ import Language.PureScript.Types
import Language.PureScript.Label (Label(..))
import Language.PureScript.PSString (PSString)

import Debug.Trace
import Language.PureScript.CoreFn.Pretty.Types (prettyTypeStr)
import Language.PureScript.Pretty.Values (renderValue)

moduleTraces :: Bool
moduleTraces = True

goTrace :: forall x. String -> x -> x
goTrace str x
| moduleTraces = trace str x
| otherwise = x

goTraceM :: forall f. Applicative f => String -> f ()
goTraceM msg
| moduleTraces = traceM msg
| otherwise = pure ()

spacer = '\n' : replicate 20 '-'



data BindingGroupType
= RecursiveBindingGroup
| NonRecursiveBindingGroup
Expand All @@ -102,7 +124,7 @@ typesOf
-> ModuleName
-> [((SourceAnn, Ident), Expr)]
-> m [((SourceAnn, Ident), (Expr, SourceType))]
typesOf bindingGroupType moduleName vals = withFreshSubstitution $ do
typesOf bindingGroupType moduleName vals = goTrace ("TYPESOF: " <> T.unpack (runModuleName moduleName)) $ withFreshSubstitution $ do
(tys, wInfer) <- capturingSubstitution tidyUp $ do
(SplitBindingGroup untyped typed dict, w) <- withoutWarnings $ typeDictionaryForBindingGroup (Just moduleName) vals
ds1 <- parU typed $ \e -> withoutWarnings $ checkTypedBindingGroupElement moduleName e dict
Expand Down Expand Up @@ -302,7 +324,7 @@ checkTypedBindingGroupElement
-> M.Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-- ^ Names brought into scope in this binding group
-> m ((SourceAnn, Ident), (Expr, SourceType))
checkTypedBindingGroupElement mn (ident, (val, args, ty, checkType)) dict = do
checkTypedBindingGroupElement mn (ident, (val, args, ty, checkType)) dict = goTrace msg $ do
-- We replace type synonyms _after_ kind-checking, since we don't want type
-- synonym expansion to bring type variables into scope. See #2542.
ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
Expand All @@ -311,6 +333,12 @@ checkTypedBindingGroupElement mn (ident, (val, args, ty, checkType)) dict = do
then withScopedTypeVars mn args $ bindNames dict $ check val ty'
else return (TypedValue' False val ty')
return (ident, (tvToExpr val', ty'))
where
msg = "CHECK_TYPED_BINDING_GROUP_ELEMENT: " <> T.unpack (runIdent $ snd ident)
<> "\n VALUE: " <> renderValue 100 val
<> "\n ARGS: " <> concatMap (\(_nm,_ty) -> " " <> T.unpack _nm <> " := " <> prettyTypeStr _ty <> "\n") args
<> "\n TYPE: " <> prettyTypeStr ty
<> spacer

-- | Infer a type for a value in a binding group which lacks an annotation.
typeForBindingGroupElement
Expand All @@ -321,12 +349,17 @@ typeForBindingGroupElement
-> M.Map (Qualified Ident) (SourceType, NameKind, NameVisibility)
-- ^ Names brought into scope in this binding group
-> m ((SourceAnn, Ident), (Expr, SourceType))
typeForBindingGroupElement (ident, (val, ty)) dict = do
typeForBindingGroupElement (ident, (val, ty)) dict = goTrace msg $ do
-- Infer the type with the new names in scope
TypedValue' _ val' ty' <- bindNames dict $ infer val
-- Unify the type with the unification variable we chose for this definition
unifyTypes ty ty'
return (ident, (TypedValue True val' ty', ty'))
where
msg = "TYPE_FOR_BINDING_GROUP_ELEMENT: " <> T.unpack (runIdent $ snd ident)
<> "\n VALUE: " <> renderValue 100 val
<> "\n TYPE: " <> prettyTypeStr ty
<> spacer

-- | Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
-- or TypeClassDictionary values.
Expand All @@ -338,14 +371,35 @@ instantiatePolyTypeWithUnknowns
=> Expr
-> SourceType
-> m (Expr, SourceType)
instantiatePolyTypeWithUnknowns val (ForAll _ _ ident mbK ty _) = do
instantiatePolyTypeWithUnknowns val printMe@(ForAll _ _ ident mbK ty _) = do
u <- freshTypeWithKind mbK
insertUnkName' u ident
instantiatePolyTypeWithUnknowns val $ replaceTypeVars ident u ty
instantiatePolyTypeWithUnknowns val (ConstrainedType _ con ty) = do
result <- instantiatePolyTypeWithUnknowns val $ replaceTypeVars ident u ty
let msg = mkMsg result
goTraceM msg
pure result
where
mkMsg (resultExpr,resultTy)
= "INSTANTIATE POLYTYPES WITH UNKNOWNS"
<> "\n EXPR: " <> renderValue 100 val
<> "\n TYPE: " <> prettyTypeStr printMe
<> "\n RESULT EXPR: " <> renderValue 100 resultExpr
<> "\n RESULT TYPE: " <> prettyTypeStr resultTy
<> spacer
instantiatePolyTypeWithUnknowns val printMe@(ConstrainedType _ con ty) = do
dicts <- getTypeClassDictionaries
hints <- getHints
instantiatePolyTypeWithUnknowns (App val (TypeClassDictionary con dicts hints)) ty
result <- instantiatePolyTypeWithUnknowns (App val (TypeClassDictionary con dicts hints)) ty
goTraceM (mkMsg result)
pure result
where
mkMsg (resultExpr,resultTy)
= "INSTANTIATE POLYTYPES WITH UNKNOWNS"
<> "\n EXPR: " <> renderValue 100 val
<> "\n TYPE: " <> prettyTypeStr printMe
<> "\n RESULT EXPR: " <> renderValue 100 resultExpr
<> "\n RESULT TYPE: " <> prettyTypeStr resultTy
<> spacer
instantiatePolyTypeWithUnknowns val ty = return (val, ty)

instantiatePolyTypeWithUnknownsUntilVisible
Expand All @@ -368,15 +422,20 @@ instantiateConstraint val ty = pure (val, ty)

-- | Match against TUnknown and call insertUnkName, failing otherwise.
insertUnkName' :: (MonadState CheckState m, MonadError MultipleErrors m) => SourceType -> Text -> m ()
insertUnkName' (TUnknown _ i) n = insertUnkName i n
insertUnkName' tu@(TUnknown _ i) n = goTrace msg $ insertUnkName i n
where
msg = "INSERT UNK NAME"
<> "\n TYPE: " <> prettyTypeStr tu
<> "\n NAME: " <> T.unpack n
insertUnkName' _ _ = internalCompilerError "type is not TUnknown"

-- | Infer a type for a value, rethrowing any error to provide a more useful error message
infer
:: (MonadSupply m, MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
=> Expr
-> m TypedValue'
infer val = withErrorMessageHint (ErrorInferringType val) $ infer' val
infer val = goTrace ("INFER\n EXPR: " <> renderValue 100 val <> spacer)
withErrorMessageHint (ErrorInferringType val) $ infer' val

-- | Infer a type for a value
infer'
Expand Down Expand Up @@ -772,7 +831,16 @@ check
=> Expr
-> SourceType
-> m TypedValue'
check val ty = withErrorMessageHint' val (ErrorCheckingType val ty) $ check' val ty
check val ty = do
goTraceM msg1
result <- withErrorMessageHint' val (ErrorCheckingType val ty) $ check' val ty
let msg2 = "\n CHECK RESULT: " <> renderValue 100 (tvToExpr result) <> spacer
goTraceM msg2
pure result
where
msg1 = "CHECK"
<> "\n EXPR: " <> renderValue 100 val
<> "\n TYPE: " <> prettyTypeStr ty

-- |
-- Check the type of a value
Expand Down
Loading

0 comments on commit ff0b89f

Please sign in to comment.