Merge pull request #27 from gelisam/issue-17/error-locations

proper error locations in error messages

Author: gelisam

src/TypeLevel/Rewrite.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE LambdaCase, RecordWildCards, ViewPatterns #-}
+{-# LANGUAGE LambdaCase, OverloadedStrings, RecordWildCards, ViewPatterns #-}
 module TypeLevel.Rewrite (plugin) where
 
 import Control.Monad
@@ -8,9 +8,9 @@ import Data.Foldable
 import Data.Traversable
 
 -- GHC API
-import GhcPlugins (eqType)
 import Coercion (Role(Representational), mkUnivCo)
-import Constraint (Ct, ctEvExpr, ctLoc, mkNonCanonical)
+import Constraint (CtEvidence(ctev_loc), Ct, ctEvExpr, ctLoc, mkNonCanonical)
+import GhcPlugins (PredType, SDoc, eqType, fsep, ppr)
 import Plugins (Plugin(pluginRecompile, tcPlugin), CommandLineOption, defaultPlugin, purePlugin)
 import TcEvidence (EvExpr, EvTerm, evCast)
 import TcPluginM (newWanted)
@@ -72,15 +72,17 @@ lookupTypeRules
   :: [CommandLineOption]
   -> TcPluginM [TypeRule]
 lookupTypeRules [] = do
-  usage (show ["TypeLevel.Append.RightIdentity", "TypeLevel.Append.RightAssociative"])
+  usage (show [ "TypeLevel.Append.RightIdentity" :: String
+              , "TypeLevel.Append.RightAssociative"
+              ])
         "[]"
 lookupTypeRules fullyQualifiedTypeSynonyms = do
   -- ["TypeLevel.Append.RightIdentity", "TypeLevel.Append.RightAssociative"]
   for fullyQualifiedTypeSynonyms $ \fullyQualifiedTypeSynonym -> do
     -- "TypeLevel.Append.RightIdentity"
     case splitLastDot fullyQualifiedTypeSynonym of
       Nothing -> do
-        usage (show "TypeLevel.Append.RightIdentity")
+        usage (show ("TypeLevel.Append.RightIdentity" :: String))
               (show fullyQualifiedTypeSynonym)
       Just (moduleNameStr, tyConNameStr) -> do
         -- ("TypeLevel.Append", "RightIdentity")
@@ -114,6 +116,31 @@ plugin = defaultPlugin
   }
 
 
+mkErrCtx
+  :: SDoc
+  -> ErrCtxt
+mkErrCtx errDoc = (True, \env -> pure (env, errDoc))
+
+newRuleInducedWanted
+  :: Ct
+  -> TypeRule
+  -> PredType
+  -> TcPluginM CtEvidence
+newRuleInducedWanted oldCt rule newPredType = do
+  let loc = ctLoc oldCt
+
+  -- include the rewrite rule in the error message, if any
+  let errMsg = fsep [ "From the typelevel rewrite rule:"
+                    , ppr (fromTypeRule rule)
+                    ]
+  let loc' = pushErrCtxtSameOrigin (mkErrCtx errMsg) loc
+
+  wanted <- newWanted loc' newPredType
+
+  -- ctLoc only copies the "arising from function X" part but not the location
+  -- etc., so we need to copy the rest of it manually
+  pure $ wanted { ctev_loc = loc' }
+
 solve
   :: [TypeRule]
   -> [Ct]  -- ^ Given constraints
@@ -142,27 +169,27 @@ solve rules givens _ wanteds = do
         let typeTerms = fmap toTypeTerm types
         let predType = fromDecomposeConstraint types
 
-        -- C a' b' c'
-        let typeTerms' = fmap (applyRules typeSubst rules) typeTerms
-        let types' = fmap fromTypeTerm typeTerms'
-        let predType' = fromDecomposeConstraint types'
-
-        unless (eqType predType' predType) $ do
-          -- co :: C a' b' c'  ~R  C a b c
-          let co = mkUnivCo
-                     (PluginProv "TypeLevel.Rewrite")
-                     Representational
-                     predType'
-                     predType
-          evWanted' <- lift $ newWanted (ctLoc wanted) predType'
-          let wanted' = mkNonCanonical evWanted'
-          let futureDict :: EvExpr
-              futureDict = ctEvExpr evWanted'
-          let replaceCt :: ReplaceCt
-              replaceCt = ReplaceCt
-                { evidenceOfCorrectness  = evCast futureDict co
-                , replacedConstraint     = wanted
-                , replacementConstraints = [wanted']
-                }
-          tell [replaceCt]
+        for_ (applyRules typeSubst rules typeTerms) $ \(rule, typeTerms') -> do
+          -- C a' b' c'
+          let types' = fmap fromTypeTerm typeTerms'
+          let predType' = fromDecomposeConstraint types'
+
+          unless (eqType predType' predType) $ do
+            -- co :: C a' b' c'  ~R  C a b c
+            let co = mkUnivCo
+                       (PluginProv "TypeLevel.Rewrite")
+                       Representational
+                       predType'
+                       predType
+            evWanted' <- lift $ newRuleInducedWanted wanted rule predType'
+            let wanted' = mkNonCanonical evWanted'
+            let futureDict :: EvExpr
+                futureDict = ctEvExpr evWanted'
+            let replaceCt :: ReplaceCt
+                replaceCt = ReplaceCt
+                  { evidenceOfCorrectness  = evCast futureDict co
+                  , replacedConstraint     = wanted
+                  , replacementConstraints = [wanted']
+                  }
+            tell [replaceCt]
   pure $ combineReplaceCts replaceCts

src/TypeLevel/Rewrite/Internal/ApplyRules.hs

@@ -1,13 +1,14 @@
-{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE LambdaCase, TupleSections, ViewPatterns #-}
 {-# OPTIONS -Wno-name-shadowing #-}
 module TypeLevel.Rewrite.Internal.ApplyRules where
 
 import Control.Applicative
 import Control.Monad
+import Control.Monad.Trans.Class
 import Control.Monad.Trans.State
 import Data.Foldable (asum, for_)
 import Data.Map (Map)
-import Data.Maybe (isJust)
+import Data.Maybe (listToMaybe, maybeToList)
 import Data.Traversable
 import qualified Data.Map as Map
 
@@ -27,37 +28,25 @@ import TypeLevel.Rewrite.Internal.TypeSubst
 import TypeLevel.Rewrite.Internal.TypeTerm
 
 
+type Subst = Map TyVar (Term TypeNode TypeEq)
+
 applyRules
-  :: TypeSubst
+  :: Traversable t
+  => TypeSubst
   -> [TypeRule]
-  -> TypeTerm
-  -> TypeTerm
-applyRules _ []
-  = id
-applyRules typeSubst rules
-  = go (length rules * 100)
-  where
-    go :: Int -> TypeTerm -> TypeTerm
-    go 0 _
-      = error "the rewrite rules form a cycle"
-    go fuel typeTerm
-      = case multiRewrite typeSubst rules typeTerm of
-          Nothing
-            -> typeTerm
-          Just typeTerm'
-            -> go (fuel - 1) typeTerm'
-
-
-type Subst = Map TyVar (Term TypeNode TypeEq)
+  -> t TypeTerm
+  -> Maybe (TypeRule,t TypeTerm)
+applyRules typeSubst rules inputs
+  = annotatedTraverseFirst (multiRewrite typeSubst rules) inputs
 
 multiRewrite
   :: TypeSubst
   -> [TypeRule]
   -> TypeTerm
-  -> Maybe TypeTerm
+  -> Maybe (TypeRule, TypeTerm)
 multiRewrite typeSubst rules input
   = asum
-    [ singleRewrite typeSubst rule input
+    [ (rule,) <$> singleRewrite typeSubst rule input
     | rule <- rules
     ]
 
@@ -70,7 +59,7 @@ singleRewrite
   -> Maybe TypeTerm
 singleRewrite typeSubst rule input@(Fun inputF inputXS)
     = topLevelRewrite typeSubst rule input
-  <|> zipRewrite inputF inputXS (fmap (singleRewrite typeSubst rule) inputXS)
+  <|> (Fun inputF <$> traverseFirst (singleRewrite typeSubst rule) inputXS)
 singleRewrite typeSubst rule input
   = topLevelRewrite typeSubst rule input
 
@@ -110,17 +99,57 @@ topLevelRewrite typeSubst (Rule pattern0 pattern') input0 = do
                                $ typeSubst
       asum $ fmap (go pattern) possibleReplacements
 
--- >>> zipRewrite F [x,y,z] [Nothing,Nothing,Nothing]
+-- >>> traverseFirst (\x -> if even x then Just (10 + x) else Nothing) [1,3,5]
 -- Nothing
--- >>> zipRewrite F [x,y,z] [Just x',Nothing,Just z']
--- Just [x',y,z']
-zipRewrite
-  :: TypeNode
-  -> [TypeTerm]
-  -> [Maybe TypeTerm]
-  -> Maybe TypeTerm
-zipRewrite f inputXS intermediateXS = do
-  guard (any isJust intermediateXS)
-  outputXS <- for (zip inputXS intermediateXS) $ \(input, intermediate) -> do
-    intermediate <|> pure input
-  pure $ Fun f outputXS
+-- >>> traverseFirst (\x -> if even x then Just (10 + x) else Nothing) [1,2,4]
+-- Just [1,12,4]
+traverseFirst
+  :: Traversable t
+  => (a -> Maybe a)
+  -> t a
+  -> Maybe (t a)
+traverseFirst f = listToMaybe . traverseAll f
+
+annotatedTraverseFirst
+  :: Traversable t
+  => (a -> Maybe (annotation, a))
+  -> t a
+  -> Maybe (annotation, t a)
+annotatedTraverseFirst f = listToMaybe . annotatedTraverseAll f
+
+-- >>> traverseAll (\x -> if even x then Just (10 + x) else Nothing) [1,3,5]
+-- []
+-- >>> traverseAll (\x -> if even x then Just (10 + x) else Nothing) [1,2,4]
+-- [[1,12,4], [1,2,14]]
+traverseAll
+  :: Traversable t
+  => (a -> Maybe a)
+  -> t a
+  -> [t a]
+traverseAll f
+  = fmap snd
+  . annotatedTraverseAll (fmap ((),) . f)
+
+annotatedTraverseAll
+  :: Traversable t
+  => (a -> Maybe (annotation, a))
+  -> t a
+  -> [(annotation, t a)]
+annotatedTraverseAll f ta = flip evalStateT Nothing $ do
+  ta' <- for ta $ \a -> do
+    get >>= \case
+      Just _ -> do
+        -- already picked one
+        pure a
+      Nothing -> do
+        pickIt <- lift [True,False]
+        if pickIt
+          then do
+            (annotation, a) <- lift $ maybeToList $ f a
+            put (Just annotation)
+            pure a
+          else do
+            pure a
+  maybeAnnotation <- get
+  annotation <- lift $ maybeToList maybeAnnotation
+  pure (annotation, ta')

src/TypeLevel/Rewrite/Internal/DecomposedConstraint.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveFunctor, LambdaCase, RecordWildCards, ViewPatterns #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, LambdaCase, RecordWildCards, ViewPatterns #-}
 module TypeLevel.Rewrite.Internal.DecomposedConstraint where
 
 import Control.Applicative
@@ -12,7 +12,7 @@ import Predicate (EqRel(NomEq), Pred(ClassPred, EqPred), classifyPredType, mkCla
 data DecomposedConstraint a
   = EqualityConstraint a a        -- lhs ~ rhs
   | InstanceConstraint Class [a]  -- C a b c
-  deriving Functor
+  deriving (Functor, Foldable, Traversable)
 
 asEqualityConstraint
   :: Ct

src/TypeLevel/Rewrite/Internal/TypeNode.hs

@@ -3,7 +3,7 @@ module TypeLevel.Rewrite.Internal.TypeNode where
 
 -- GHC API
 import TyCon (TyCon)
-import Type (Type, isNumLitTy, isStrLitTy, splitTyConApp_maybe)
+import Type (Type, isNumLitTy, isStrLitTy, mkTyConApp, splitTyConApp_maybe)
 
 import TypeLevel.Rewrite.Internal.TypeEq
 
@@ -26,3 +26,10 @@ toTypeNodeApp_maybe tyLit@(isStrLitTy -> Just _)
   = pure (TyLit (TypeEq tyLit), [])
 toTypeNodeApp_maybe _
   = Nothing
+
+fromTypeNode
+  :: TypeNode
+  -> [Type]
+  -> Type
+fromTypeNode (TyCon tyCon) args = mkTyConApp tyCon args
+fromTypeNode (TyLit (TypeEq tyLit)) _ = tyLit

src/TypeLevel/Rewrite/Internal/TypeRule.hs

@@ -1,10 +1,11 @@
-{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE LambdaCase, ViewPatterns #-}
 {-# OPTIONS -Wno-name-shadowing #-}
 module TypeLevel.Rewrite.Internal.TypeRule where
 
 -- GHC API
 import Name (getOccString)
-import Type (TyVar, Type)
+import Predicate (mkPrimEqPred)
+import Type (TyVar, Type, mkTyVarTy)
 
 -- term-rewriting API
 import Data.Rewriting.Rule (Rule(..))
@@ -23,3 +24,27 @@ toTypeRule_maybe (toTypeTemplate_maybe -> Just (Fun (TyCon (getOccString -> "~")
   = Just (Rule lhs_ rhs_)
 toTypeRule_maybe _
   = Nothing
+
+fromTyVar
+  :: TyVar
+  -> Type
+fromTyVar
+  = mkTyVarTy
+
+fromTerm
+  :: (f -> [Type] -> Type)
+  -> (v -> Type)
+  -> Term f v
+  -> Type
+fromTerm fromF fromV = \case
+  Var v
+    -> fromV v
+  Fun f args
+    -> fromF f (fmap (fromTerm fromF fromV) args)
+
+fromTypeRule
+  :: TypeRule
+  -> Type
+fromTypeRule (Rule lhs rhs)
+  = mkPrimEqPred (fromTerm fromTypeNode fromTyVar lhs)
+                 (fromTerm fromTypeNode fromTyVar rhs)

test/error-messages-cases/error-location/expected

@@ -0,0 +1,8 @@
+<path>/error-messages-cases/error-location/src/ErrorLocation/Test.hs:13:5: error:
+    • No instance for (Foo (F a b)) arising from a use of ‘foo’
+    • From the typelevel rewrite rule: F x (F x y) ~ F x y
+      In the expression: foo @(F a (F a b))
+      In an equation for ‘f’: f = foo @(F a (F a b))
+   |
+13 | f = foo @(F a (F a b))
+   |     ^^^^^^^^^^^^^^^^^^

test/error-messages-cases/error-location/package.yaml

@@ -0,0 +1,7 @@
+dependencies:
+  - base
+  - typelevel-rewrite-rules
+
+library:
+  source-dirs:      src
+  ghc-options: -W -Wall

test/error-messages-cases/error-location/src/ErrorLocation/Laws.hs

@@ -0,0 +1,6 @@
+{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
+module ErrorLocation.Laws where
+
+type family F a b
+
+type FLaw x y = F x (F x y) ~ F x y

test/error-messages-cases/error-location/src/ErrorLocation/Test.hs

@@ -0,0 +1,13 @@
+{-# LANGUAGE AllowAmbiguousTypes, FlexibleContexts, ScopedTypeVariables, TypeApplications, TypeFamilies #-}
+{-# OPTIONS_GHC -fplugin TypeLevel.Rewrite
+                -fplugin-opt=TypeLevel.Rewrite:ErrorLocation.Laws.FLaw #-}
+module ErrorLocation.Test where
+
+import ErrorLocation.Laws
+
+
+class Foo a where
+  foo :: ()
+
+f :: forall a b. ()
+f = foo @(F a (F a b))