Drop UnusableDeclaration; update NoInstanceFound error (#4513)

With the advent of visible type applications (VTAs), all type class instances 
can be determined via VTAs. This PR removes the `UnusableDeclaration` error. 
Whereas before, the code would throw the above error when type variables 
in the type class head are not mentioned in the type class member's type 
signature, now we simply track these "VTA-required" args. 
These args represent type variables that must be disambiguated using VTAs.
If VTAs are used, the instance should be found. If they are not used,
an updated `NoInstanceFound` error is thrown that notifies the user of these
"VTA-required" args if possible.

When a `NoInstanceFound` error is thrown, we do not attempt to do anything
other than notify the user of the "VTA-required" args. In a previous and 
problematic approach, we did try to do more but found a number of difficult
problems with this approach:
- Suggesting a correct usage of `coerce` with VTAs in all of its complex cases
- When a user does supply a VTA arg, assuming that that arg refers to a corresponding 
    type in a valid type class instance: `foo @Int` when there is no `Foo Int` instance
- User confusion due to a difference in order of VTA args with their usage within 
    the type class member's type signature: `foo @1 @2` when `foo :: forall one two. two -> one`

A side effect of dropping the `UnusableDeclaration` error is a scoping bug 
that was revealed in `moveQuantifiersToFront`. This bug has also been fixed.

Other notes:
- `replaceAllTypeSynonymsM` is removed as it's no longer used by anything.
- The Externs files do not store the "VTA-required" args and instead recompute them after being loaded.
- The "VTA-required" args are tracked via their indices so as to print them in their corresponding order later.

CHANGELOG.d/bug_fix-moveQuantifiersToFront-scoping.md

@@ -0,0 +1,23 @@
+* Fix scoping issues in `moveQuantifiersToFront`
+
+As a side effect of replacing `UnusableDeclaration` with
+an updated `NoInstanceFound` error, a bug appeared in how
+scoping is handled when constraints are involved.
+
+```purs
+--        | a0
+class Foo a where
+--              | a1
+  foo :: forall a. a
+```
+Before this fix, `foo`'s type signature was being transformed to
+`foo :: forall @a a. Foo a => a`
+where two type variables with the same identifier 
+are present rather than the correct signature of
+`foo :: forall @a0. Foo a0 => (forall a1. a1)`.
+
+With this fix, the above type class declaration
+will now compile and trigger a `ShadowedName` 
+warning since the type class member's `a` 
+(i.e. `a1` above) shadows the type class head's `a` 
+(i.e. `a0` above).

CHANGELOG.d/feature_replace-unused-declarations.md

@@ -0,0 +1,71 @@
+* Replace `UnusableDeclaration` with updated `NoInstanceFound`
+
+  Previously, the following type class would be invalid
+  because there was no way for the compiler to infer
+  which type class instance to select because
+  the type variable in the class head `a` was
+  not mentioned in `bar`'s type signature:
+
+  ```purs
+  class Foo a where
+    bar :: Int
+  ```
+
+  The recently-added visible type applications (VTAs)
+  can now be used to guide the compiler in such cases:
+
+  ```purs
+  class Foo a where bar :: Int
+  instance Foo String where bar = 0
+  someInt = bar @String -- use the `String` instance
+  ```
+
+  Without VTAs, the compiler
+  will still produce an `InstanceNotFound` error, but this error 
+  has been updated to note which type variables in the class head
+  can only be disambiguated via visible type applications.
+  Given the following code
+
+  ```purs
+  class Single tyVarDoesNotAppearInBody where 
+    useSingle :: Int
+
+  single :: Int
+  single = useSingle
+  ```
+
+  The error reported for `useSingle` will be:
+
+  ```
+  No type class instance was found for
+
+    Main.Single t0
+
+  The instance head contains unknown type variables.
+  
+
+  Note: The following type class members found in the expression require visible type applications 
+  to be unambiguous (e.g. tyClassMember @Int).
+    Main.useSingle
+      tyNotAppearInBody
+  ```
+
+  For a multiparameter typeclass with functional dependencies...
+
+  ```purs
+  class MultiFdBidi a b | a -> b, b -> a where
+    useMultiFdBidi :: Int
+
+  multiFdBidi :: Int
+  multiFdBidi = useMultiFdBidi
+  ```
+
+  ...the "Note" part is updated to read
+  ```
+  Note: The following type class members found in the expression require visible type applications 
+  to be unambiguous (e.g. tyClassMember @Int).
+    Main.useMultiFdBidi
+      One of the following sets of type variables:
+        a
+        b
+  ```

src/Language/PureScript/AST/Declarations.hs

@@ -103,6 +103,17 @@ data HintCategory
   | OtherHint
   deriving (Show, Eq)
 
+-- |
+-- In constraint solving, indicates whether there were `TypeUnknown`s that prevented
+-- an instance from being found, and whether VTAs are required 
+-- due to type class members not referencing all the type class
+-- head's type variables.
+data UnknownsHint
+  = NoUnknowns
+  | Unknowns
+  | UnknownsWithVtaRequiringArgs (NEL.NonEmpty (Qualified Ident, [[Text]]))
+  deriving (Show)
+
 -- |
 -- A module declaration, consisting of comments about the module, a module name,
 -- a list of declarations, and a list of the declarations that are

src/Language/PureScript/Docs/Convert/ReExports.hs

@@ -441,7 +441,7 @@ handleEnv TypeClassEnv{..} =
           ++ T.unpack cdeclTitle)
 
   addConstraint constraint =
-    P.quantify . P.moveQuantifiersToFront . P.ConstrainedType () constraint
+    P.quantify . P.moveQuantifiersToFront () . P.ConstrainedType () constraint
 
 splitMap :: Map k (v1, v2) -> (Map k v1, Map k v2)
 splitMap = fmap fst &&& fmap snd

src/Language/PureScript/Environment.hs

@@ -14,7 +14,7 @@ import Data.IntMap qualified as IM
 import Data.IntSet qualified as IS
 import Data.Map qualified as M
 import Data.Set qualified as S
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Semigroup (First(..))
 import Data.Text (Text)
 import Data.Text qualified as T
@@ -25,7 +25,7 @@ import Language.PureScript.Crash (internalError)
 import Language.PureScript.Names (Ident, ProperName(..), ProperNameType(..), Qualified, QualifiedBy, coerceProperName)
 import Language.PureScript.Roles (Role(..))
 import Language.PureScript.TypeClassDictionaries (NamedDict)
-import Language.PureScript.Types (SourceConstraint, SourceType, Type(..), TypeVarVisibility(..), eqType, srcTypeConstructor)
+import Language.PureScript.Types (SourceConstraint, SourceType, Type(..), TypeVarVisibility(..), eqType, srcTypeConstructor, freeTypeVariables)
 import Language.PureScript.Constants.Prim qualified as C
 
 -- | The @Environment@ defines all values and types which are currently in scope:
@@ -54,9 +54,10 @@ data TypeClassData = TypeClassData
   { typeClassArguments :: [(Text, Maybe SourceType)]
   -- ^ A list of type argument names, and their kinds, where kind annotations
   -- were provided.
-  , typeClassMembers :: [(Ident, SourceType)]
-  -- ^ A list of type class members and their types. Type arguments listed above
-  -- are considered bound in these types.
+  , typeClassMembers :: [(Ident, SourceType, Maybe (S.Set (NEL.NonEmpty Int)))]
+  -- ^ A list of type class members and their types and whether or not
+  -- they have type variables that must be defined using Visible Type Applications.
+  -- Type arguments listed above are considered bound in these types.
   , typeClassSuperclasses :: [SourceConstraint]
   -- ^ A list of superclasses of this type class. Type arguments listed above
   -- are considered bound in the types appearing in these constraints.
@@ -129,10 +130,23 @@ makeTypeClassData
   -> [FunctionalDependency]
   -> Bool
   -> TypeClassData
-makeTypeClassData args m s deps = TypeClassData args m s deps determinedArgs coveringSets
+makeTypeClassData args m s deps = TypeClassData args m' s deps determinedArgs coveringSets
   where
     ( determinedArgs, coveringSets ) = computeCoveringSets (length args) deps
 
+    coveringSets' = S.toList coveringSets
+
+    m' = map (\(a, b) -> (a, b, addVtaInfo b)) m
+
+    addVtaInfo :: SourceType -> Maybe (S.Set (NEL.NonEmpty Int))
+    addVtaInfo memberTy = do
+      let mentionedArgIndexes = S.fromList (mapMaybe argToIndex $ freeTypeVariables memberTy)
+      let leftovers = map (`S.difference` mentionedArgIndexes) coveringSets'
+      S.fromList <$> traverse (NEL.nonEmpty . S.toList) leftovers
+
+    argToIndex :: Text -> Maybe Int
+    argToIndex = flip M.lookup $ M.fromList (zipWith ((,) . fst) args [0..])
+
 -- A moving frontier of sets to consider, along with the fundeps that can be
 -- applied in each case. At each stage, all sets in the frontier will be the
 -- same size, decreasing by 1 each time.

src/Language/PureScript/Errors.hs

@@ -111,7 +111,7 @@ data SimpleErrorMessage
   | NoInstanceFound
       SourceConstraint -- ^ constraint that could not be solved
       [Qualified (Either SourceType Ident)] -- ^ a list of instances that stopped further progress in instance chains due to ambiguity
-      Bool -- ^ whether eliminating unknowns with annotations might help
+      UnknownsHint -- ^ whether eliminating unknowns with annotations might help or if visible type applications are required
   | AmbiguousTypeVariables SourceType [(Text, Int)]
   | UnknownClass (Qualified (ProperName 'ClassName))
   | PossiblyInfiniteInstance (Qualified (ProperName 'ClassName)) [SourceType]
@@ -177,8 +177,6 @@ data SimpleErrorMessage
   | ClassInstanceArityMismatch Ident (Qualified (ProperName 'ClassName)) Int Int
   -- | a user-defined warning raised by using the Warn type class
   | UserDefinedWarning SourceType
-  -- | a declaration couldn't be used because it contained free variables
-  | UnusableDeclaration Ident [[Text]]
   | CannotDefinePrimModules ModuleName
   | MixedAssociativityError (NEL.NonEmpty (Qualified (OpName 'AnyOpName), Associativity))
   | NonAssociativeError (NEL.NonEmpty (Qualified (OpName 'AnyOpName)))
@@ -352,7 +350,6 @@ errorCode em = case unwrapErrorMessage em of
   CannotUseBindWithDo{} -> "CannotUseBindWithDo"
   ClassInstanceArityMismatch{} -> "ClassInstanceArityMismatch"
   UserDefinedWarning{} -> "UserDefinedWarning"
-  UnusableDeclaration{} -> "UnusableDeclaration"
   CannotDefinePrimModules{} -> "CannotDefinePrimModules"
   MixedAssociativityError{} -> "MixedAssociativityError"
   NonAssociativeError{} -> "NonAssociativeError"
@@ -917,7 +914,8 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
             , line ("You can use " <> markCode "_ <- ..." <> " to explicitly discard the result.")
             ]
     renderSimpleErrorMessage (NoInstanceFound (Constraint _ nm _ ts _) ambiguous unks) =
-      paras [ line "No type class instance was found for"
+      paras $
+            [ line "No type class instance was found for"
             , markCodeBox $ indent $ Box.hsep 1 Box.left
                 [ line (showQualified runProperName nm)
                 , Box.vcat Box.left (map prettyTypeAtom ts)
@@ -930,10 +928,32 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
                         [] -> []
                         [_] -> useMessage "The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered:"
                         _ -> useMessage "The following instances partially overlap the above constraint, which means the rest of their instance chains will not be considered:"
-            , paras [ line "The instance head contains unknown type variables. Consider adding a type annotation."
-                    | unks
-                    ]
-            ]
+            ] <> case unks of
+                  NoUnknowns ->
+                    []
+                  Unknowns ->
+                    [ line "The instance head contains unknown type variables. Consider adding a type annotation." ]
+                  UnknownsWithVtaRequiringArgs tyClassMembersRequiringVtas ->
+                    let
+                      renderSingleTyClassMember (tyClassMember, argsRequiringVtas) =
+                        Box.moveRight 2 $ paras $
+                          [ line $ markCode (showQualified showIdent tyClassMember) ]
+                          <> case argsRequiringVtas of
+                              [required] ->
+                                [ Box.moveRight 2 $ line $ T.intercalate ", " required ]
+                              options -> 
+                                [ Box.moveRight 2 $ line "One of the following sets of type variables:"
+                                , Box.moveRight 2 $ paras $
+                                    map (\set -> Box.moveRight 2 $ line $ T.intercalate ", " set) options
+                                ]
+                    in
+                      [ paras
+                        [ line "The instance head contains unknown type variables."
+                        , Box.moveDown 1 $ paras $
+                            [ line $ "Note: The following type class members found in the expression require visible type applications to be unambiguous (e.g. " <> markCode "tyClassMember @Int" <> ")."]
+                            <> map renderSingleTyClassMember (NEL.toList tyClassMembersRequiringVtas)
+                        ]
+                      ]
     renderSimpleErrorMessage (AmbiguousTypeVariables t uis) =
       paras [ line "The inferred type"
             , markCodeBox $ indent $ prettyType t
@@ -1277,22 +1297,6 @@ prettyPrintSingleError (PPEOptions codeColor full level showDocs relPath fileCon
             , indent msg
             ]
 
-    renderSimpleErrorMessage (UnusableDeclaration ident unexplained) =
-      paras $
-        [ line $ "The declaration " <> markCode (showIdent ident) <> " contains arguments that couldn't be determined."
-        ] <>
-
-        case unexplained of
-          [required] ->
-            [ line $ "These arguments are: { " <> T.intercalate ", " required <> " }"
-            ]
-
-          options  ->
-            [ line "To fix this, one of the following sets of variables must be determined:"
-            , Box.moveRight 2 . Box.vsep 0 Box.top $
-                map (\set -> line $ "{ " <> T.intercalate ", " set <> " }") options
-            ]
-
     renderSimpleErrorMessage (CannotDefinePrimModules mn) =
       paras
         [ line $ "The module name " <> markCode (runModuleName mn) <> " is in the Prim namespace."

src/Language/PureScript/Externs.hs

@@ -254,7 +254,7 @@ moduleToExternsFile (Module ss _ mn ds (Just exps)) env renamedIdents = ExternsF
     = [ EDType (coerceProperName className) kind tk
       , EDType dictName dictKind dictData
       , EDDataConstructor dctor dty dictName ty args
-      , EDClass className typeClassArguments typeClassMembers typeClassSuperclasses typeClassDependencies typeClassIsEmpty
+      , EDClass className typeClassArguments ((\(a, b, _) -> (a, b)) <$> typeClassMembers) typeClassSuperclasses typeClassDependencies typeClassIsEmpty
       ]
   toExternsDeclaration (TypeInstanceRef ss' ident ns)
     = [ EDInstance tcdClassName (lookupRenamedIdent ident) tcdForAll tcdInstanceKinds tcdInstanceTypes tcdDependencies tcdChain tcdIndex ns ss'

src/Language/PureScript/Interactive/Printer.hs

@@ -69,7 +69,7 @@ printModuleSignatures moduleName P.Environment{..} =
                     textT (P.runProperName name)
                     Box.<> textT (foldMap ((" " <>) . fst) typeClassArguments)
                 classBody =
-                    Box.vcat Box.top (map (\(i, t) -> textT (P.showIdent i <> " ::") Box.<+> P.typeAsBox maxBound t) typeClassMembers)
+                    Box.vcat Box.top (map (\(i, t, _) -> textT (P.showIdent i <> " ::") Box.<+> P.typeAsBox maxBound t) typeClassMembers)
 
             in
               Just $

src/Language/PureScript/Sugar/TypeClasses.hs

@@ -305,7 +305,7 @@ typeClassMemberToDictionaryAccessor mn name args (TypeDeclaration (TypeDeclarati
   in ValueDecl sa ident Private []
     [MkUnguarded (
      TypedValue False (Abs (VarBinder ss dictIdent) (Case [Var ss $ Qualified ByNullSourcePos dictIdent] [CaseAlternative [ctor] [MkUnguarded acsr]])) $
-       addVisibility visibility (moveQuantifiersToFront (quantify (srcConstrainedType (srcConstraint className [] (map (srcTypeVar . fst) args) Nothing) ty)))
+       addVisibility visibility (moveQuantifiersToFront NullSourceAnn (quantify (srcConstrainedType (srcConstraint className [] (map (srcTypeVar . fst) args) Nothing) ty)))
     )]
 typeClassMemberToDictionaryAccessor _ _ _ _ = internalError "Invalid declaration in type class definition"
 
@@ -333,7 +333,7 @@ typeInstanceDictionaryDeclaration sa@(ss, _) name mn deps className tys decls =
       M.lookup (qualify mn className) m
 
   -- Replace the type arguments with the appropriate types in the member types
-  let memberTypes = map (second (replaceAllTypeVars (zip (map fst typeClassArguments) tys))) typeClassMembers
+  let memberTypes = map (second (replaceAllTypeVars (zip (map fst typeClassArguments) tys)) . tuple3To2) typeClassMembers
 
   let declaredMembers = S.fromList $ mapMaybe declIdent decls
 
@@ -386,3 +386,6 @@ superClassDictionaryNames supers =
   [ superclassName pn index
   | (index, Constraint _ pn _ _ _) <- zip [0..] supers
   ]
+
+tuple3To2 :: (a, b, c) -> (a, b)
+tuple3To2 (a, b, _) = (a, b)

src/Language/PureScript/TypeChecker.hs

@@ -18,7 +18,7 @@ import Control.Monad.Supply.Class (MonadSupply)
 import Control.Monad.Writer.Class (MonadWriter, tell)
 
 import Data.Foldable (for_, traverse_, toList)
-import Data.List (nub, nubBy, (\\), sort, group)
+import Data.List (nubBy, (\\), sort, group)
 import Data.Maybe (fromMaybe, listToMaybe, mapMaybe)
 import Data.Either (partitionEithers)
 import Data.Text (Text)
@@ -45,7 +45,7 @@ import Language.PureScript.TypeChecker.Synonyms as T
 import Language.PureScript.TypeChecker.Types as T
 import Language.PureScript.TypeChecker.Unify (varIfUnknown)
 import Language.PureScript.TypeClassDictionaries (NamedDict, TypeClassDictionaryInScope(..))
-import Language.PureScript.Types (Constraint(..), SourceConstraint, SourceType, Type(..), containsForAll, eqType, everythingOnTypes, freeTypeVariables, overConstraintArgs, srcInstanceType, unapplyTypes)
+import Language.PureScript.Types (Constraint(..), SourceConstraint, SourceType, Type(..), containsForAll, eqType, everythingOnTypes, overConstraintArgs, srcInstanceType, unapplyTypes)
 
 addDataType
   :: (MonadState CheckState m, MonadError MultipleErrors m, MonadWriter MultipleErrors m)
@@ -161,7 +161,6 @@ addTypeClass _ qualifiedClassName args implies dependencies ds kind = do
       hasSig = qualName `M.member` types env
   unless (hasSig || not (containsForAll kind)) $ do
     tell . errorMessage $ MissingKindDeclaration ClassSig (disqualify qualName) kind
-  traverse_ (checkMemberIsUsable newClass (typeSynonyms env) (types env)) classMembers
   putEnv $ env { types = M.insert qualName (kind, ExternData (nominalRolesForKind kind)) (types env)
                , typeClasses = M.insert qualifiedClassName newClass (typeClasses env) }
   where
@@ -179,30 +178,9 @@ addTypeClass _ qualifiedClassName args implies dependencies ds kind = do
         Just tcd -> tcd
         Nothing -> internalError "Unknown super class in TypeClassDeclaration"
 
-    coveringSets :: TypeClassData -> [S.Set Int]
-    coveringSets = S.toList . typeClassCoveringSets
-
-    argToIndex :: Text -> Maybe Int
-    argToIndex = flip M.lookup $ M.fromList (zipWith ((,) . fst) args [0..])
-
     toPair (TypeDeclaration (TypeDeclarationData _ ident ty)) = (ident, ty)
     toPair _ = internalError "Invalid declaration in TypeClassDeclaration"
 
-    -- Currently we are only checking usability based on the type class currently
-    -- being defined.  If the mentioned arguments don't include a covering set,
-    -- then we won't be able to find a instance.
-    checkMemberIsUsable :: TypeClassData -> T.SynonymMap -> T.KindMap -> (Ident, SourceType) -> m ()
-    checkMemberIsUsable newClass syns kinds (ident, memberTy) = do
-      memberTy' <- T.replaceAllTypeSynonymsM syns kinds memberTy
-      let mentionedArgIndexes = S.fromList (mapMaybe argToIndex (freeTypeVariables memberTy'))
-      let leftovers = map (`S.difference` mentionedArgIndexes) (coveringSets newClass)
-
-      unless (any null leftovers) . throwError . errorMessage $
-        let
-          solutions = map (map (fst . (args !!)) . S.toList) leftovers
-        in
-          UnusableDeclaration ident (nub solutions)
-
 addTypeClassDictionaries
   :: (MonadState CheckState m)
   => QualifiedBy