From d7c69db126f3f317a9fc5c829a524f95e2df056a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Thu, 5 Sep 2024 10:57:30 +0200 Subject: [PATCH] Fix locations in Internal hole substitution (only for the case of substituting identifiers) (#2995) Type checking messes up the locations by substituting the holes (instance holes and ordinary holes) without adjusting the location of the expression substituted into the hole. Instead, the location of the expression substituted into the hole is preserved. This messes up locations in type-checked Internal, because the substituted expressions can come from anywhere. Later on, the error locations are wrong in Core, and get wrongly displayed e.g. for pattern matching coverage errors. This PR implements a partial solution for the (most common) case when the substituted expression is an identifier. In the future, we should have a general solution to preserve the hole locations. --- src/Juvix/Compiler/Internal/Builtins.hs | 2 +- src/Juvix/Compiler/Internal/Data/Name.hs | 10 +++---- src/Juvix/Compiler/Internal/Data/TypedIden.hs | 12 ++++++++ src/Juvix/Compiler/Internal/Extra.hs | 15 ++++++++-- .../Compiler/Internal/Extra/CoercionInfo.hs | 10 ++++--- .../Compiler/Internal/Extra/InstanceInfo.hs | 10 ++++--- .../Analysis/TypeChecking/CheckerNew.hs | 18 +++++------ .../Analysis/TypeChecking/Traits/Resolver.hs | 30 ++++++++++++------- .../Store/Internal/Data/CoercionInfo.hs | 2 +- .../Store/Internal/Data/InstanceInfo.hs | 2 +- 10 files changed, 74 insertions(+), 37 deletions(-) create mode 100644 src/Juvix/Compiler/Internal/Data/TypedIden.hs diff --git a/src/Juvix/Compiler/Internal/Builtins.hs b/src/Juvix/Compiler/Internal/Builtins.hs index e32c62372..909976d71 100644 --- a/src/Juvix/Compiler/Internal/Builtins.hs +++ b/src/Juvix/Compiler/Internal/Builtins.hs @@ -44,7 +44,7 @@ getBuiltinName :: Interval -> a -> Sem r Name -getBuiltinName loc p = fromConcreteSymbol <$> getBuiltinSymbolHelper loc (toBuiltinPrim p) +getBuiltinName loc p = fromConcreteSymbol loc <$> getBuiltinSymbolHelper loc (toBuiltinPrim p) checkBuiltinFunctionInfo :: forall r. diff --git a/src/Juvix/Compiler/Internal/Data/Name.hs b/src/Juvix/Compiler/Internal/Data/Name.hs index cbd38d342..1d2596358 100644 --- a/src/Juvix/Compiler/Internal/Data/Name.hs +++ b/src/Juvix/Compiler/Internal/Data/Name.hs @@ -103,17 +103,17 @@ type ConstrName = Name type InductiveName = Name -fromConcreteSymbol :: S.Symbol -> Name -fromConcreteSymbol s = fromConcreteSymbolPretty (S.symbolText s) s +fromConcreteSymbol :: Interval -> S.Symbol -> Name +fromConcreteSymbol loc s = fromConcreteSymbolPretty loc (S.symbolText s) s -fromConcreteSymbolPretty :: Text -> S.Symbol -> Name -fromConcreteSymbolPretty pp s = +fromConcreteSymbolPretty :: Interval -> Text -> S.Symbol -> Name +fromConcreteSymbolPretty loc pp s = Name { _nameText = S.symbolText s, _nameId = s ^. S.nameId, _nameKind = getNameKind s, _nameKindPretty = getNameKindPretty s, _namePretty = pp, - _nameLoc = getLoc (s ^. S.nameConcrete), + _nameLoc = loc, _nameFixity = s ^. S.nameFixity } diff --git a/src/Juvix/Compiler/Internal/Data/TypedIden.hs b/src/Juvix/Compiler/Internal/Data/TypedIden.hs new file mode 100644 index 000000000..123281781 --- /dev/null +++ b/src/Juvix/Compiler/Internal/Data/TypedIden.hs @@ -0,0 +1,12 @@ +module Juvix.Compiler.Internal.Data.TypedIden where + +import Juvix.Compiler.Internal.Language +import Juvix.Prelude + +data TypedIden = TypedIden + { _typedIden :: Iden, + _typedIdenType :: Expression + } + deriving stock (Data, Generic) + +makeLenses ''TypedIden diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index 8a248a836..ebefec17b 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -14,6 +14,13 @@ import Juvix.Compiler.Internal.Language import Juvix.Compiler.Store.Internal.Data.InfoTable import Juvix.Prelude +-- This is a hack to adjust location. It works only for identifiers. It should +-- change the location of an arbitrary given expression to the given location. +adjustLocation :: Interval -> Expression -> Expression +adjustLocation loc = \case + ExpressionIden iden -> ExpressionIden (set (idenName . nameLoc) loc iden) + eh -> eh + constructorArgTypes :: ConstructorInfo -> ([InductiveParameter], [FunctionParameter]) constructorArgTypes i = ( i ^. constructorInfoInductiveParameters, @@ -250,7 +257,9 @@ subsInstanceHoles s = umapM helper where helper :: Expression -> Sem r Expression helper le = case le of - ExpressionInstanceHole h -> clone (fromMaybe e (s ^. at h)) + -- TODO: The location of the hole should be preserved + ExpressionInstanceHole h -> + adjustLocation (getLoc h) <$> clone (fromMaybe e (s ^. at h)) _ -> return e where e = toExpression le @@ -260,7 +269,9 @@ subsHoles s = umapM helper where helper :: Expression -> Sem r Expression helper le = case le of - ExpressionHole h -> clone (fromMaybe e (s ^. at h)) + -- TODO: The location of the hole should be preserved + ExpressionHole h -> + adjustLocation (getLoc h) <$> clone (fromMaybe e (s ^. at h)) _ -> return e where e = toExpression le diff --git a/src/Juvix/Compiler/Internal/Extra/CoercionInfo.hs b/src/Juvix/Compiler/Internal/Extra/CoercionInfo.hs index 4210eb707..221dcd079 100644 --- a/src/Juvix/Compiler/Internal/Extra/CoercionInfo.hs +++ b/src/Juvix/Compiler/Internal/Extra/CoercionInfo.hs @@ -1,12 +1,14 @@ module Juvix.Compiler.Internal.Extra.CoercionInfo ( module Juvix.Compiler.Store.Internal.Data.CoercionInfo, module Juvix.Compiler.Internal.Extra.CoercionInfo, + module Juvix.Compiler.Internal.Data.TypedIden, ) where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet import Data.List qualified as List +import Juvix.Compiler.Internal.Data.TypedIden import Juvix.Compiler.Internal.Extra.Base import Juvix.Compiler.Internal.Extra.InstanceInfo import Juvix.Compiler.Internal.Language @@ -25,8 +27,8 @@ updateCoercionTable tab ci@CoercionInfo {..} = lookupCoercionTable :: CoercionTable -> Name -> Maybe [CoercionInfo] lookupCoercionTable tab name = HashMap.lookup name (tab ^. coercionTableMap) -coercionFromTypedExpression :: TypedExpression -> Maybe CoercionInfo -coercionFromTypedExpression TypedExpression {..} +coercionFromTypedIden :: TypedIden -> Maybe CoercionInfo +coercionFromTypedIden TypedIden {..} | null args = Nothing | otherwise = do tgt <- traitFromExpression metaVars (t ^. paramType) @@ -36,11 +38,11 @@ coercionFromTypedExpression TypedExpression {..} { _coercionInfoInductive = _instanceAppHead, _coercionInfoParams = _instanceAppArgs, _coercionInfoTarget = tgt, - _coercionInfoResult = _typedExpression, + _coercionInfoResult = _typedIden, _coercionInfoArgs = args' } where - (args, e) = unfoldFunType _typedType + (args, e) = unfoldFunType _typedIdenType args' = init args t = List.last args metaVars = HashSet.fromList $ mapMaybe (^. paramName) args' diff --git a/src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs b/src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs index 884cb0987..c9503f00e 100644 --- a/src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs +++ b/src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs @@ -1,11 +1,13 @@ module Juvix.Compiler.Internal.Extra.InstanceInfo ( module Juvix.Compiler.Store.Internal.Data.InstanceInfo, module Juvix.Compiler.Internal.Extra.InstanceInfo, + module Juvix.Compiler.Internal.Data.TypedIden, ) where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet +import Juvix.Compiler.Internal.Data.TypedIden import Juvix.Compiler.Internal.Extra.Base import Juvix.Compiler.Internal.Language import Juvix.Compiler.Store.Internal.Data.InstanceInfo @@ -99,18 +101,18 @@ traitFromExpression metaVars e = case paramFromExpression metaVars e of Just (InstanceParamApp app) -> Just app _ -> Nothing -instanceFromTypedExpression :: TypedExpression -> Maybe InstanceInfo -instanceFromTypedExpression TypedExpression {..} = do +instanceFromTypedIden :: TypedIden -> Maybe InstanceInfo +instanceFromTypedIden TypedIden {..} = do InstanceApp {..} <- traitFromExpression metaVars e return $ InstanceInfo { _instanceInfoInductive = _instanceAppHead, _instanceInfoParams = _instanceAppArgs, - _instanceInfoResult = _typedExpression, + _instanceInfoResult = _typedIden, _instanceInfoArgs = args } where - (args, e) = unfoldFunType _typedType + (args, e) = unfoldFunType _typedIdenType metaVars = HashSet.fromList $ mapMaybe (^. paramName) args checkNoMeta :: InstanceParam -> Bool diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index c18895626..987471e72 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -385,10 +385,10 @@ checkInstanceType :: checkInstanceType FunctionDef {..} = do ty <- strongNormalize _funDefType let mi = - instanceFromTypedExpression $ - TypedExpression - { _typedType = ty ^. normalizedExpression, - _typedExpression = ExpressionIden (IdenFunction _funDefName) + instanceFromTypedIden $ + TypedIden + { _typedIdenType = ty ^. normalizedExpression, + _typedIden = IdenFunction _funDefName } case mi of Just ii@InstanceInfo {..} -> do @@ -435,10 +435,10 @@ checkCoercionType :: checkCoercionType FunctionDef {..} = do ty <- strongNormalize _funDefType let mi = - coercionFromTypedExpression - ( TypedExpression - { _typedType = ty ^. normalizedExpression, - _typedExpression = ExpressionIden (IdenFunction _funDefName) + coercionFromTypedIden + ( TypedIden + { _typedIdenType = ty ^. normalizedExpression, + _typedIden = IdenFunction _funDefName } ) case mi of @@ -1109,7 +1109,7 @@ inferLeftAppExpression mhint e = case e of typedLit litt blt ty = do from <- getBuiltinNameTypeChecker i blt ihole <- freshHoleImpl i ImplicitInstance - let ty' = fromMaybe ty mhint + let ty' = maybe ty (adjustLocation i) mhint inferExpression' (Just ty') $ foldApplication (ExpressionIden (IdenFunction from)) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs index 2e4b2c296..bb7c1a151 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs @@ -41,7 +41,7 @@ resolveTraitInstance TypedHole {..} = do is <- lookupInstance ctab tab (ty ^. normalizedExpression) case is of [(cs, ii, subs)] -> - expandArity loc (subsIToE subs) (ii ^. instanceInfoArgs) (ii ^. instanceInfoResult) + expandArity' loc (subsIToE subs) (ii ^. instanceInfoArgs) (ii ^. instanceInfoResult) >>= applyCoercions loc cs [] -> throw (ErrNoInstance (NoInstance ty loc)) @@ -98,23 +98,23 @@ substitutionI subs p = case p of | otherwise -> return p -instanceFromTypedExpression' :: InfoTable -> TypedExpression -> Maybe InstanceInfo -instanceFromTypedExpression' tbl e = do - ii@InstanceInfo {..} <- instanceFromTypedExpression e +instanceFromTypedIden' :: InfoTable -> TypedIden -> Maybe InstanceInfo +instanceFromTypedIden' tbl e = do + ii@InstanceInfo {..} <- instanceFromTypedIden e guard (isTrait tbl _instanceInfoInductive) return ii varsToInstances :: InfoTable -> LocalVars -> [InstanceInfo] varsToInstances tbl LocalVars {..} = mapMaybe - (instanceFromTypedExpression' tbl . mkTyped) + (instanceFromTypedIden' tbl . mkTyped) (HashMap.toList _localTypes) where - mkTyped :: (VarName, Expression) -> TypedExpression + mkTyped :: (VarName, Expression) -> TypedIden mkTyped (v, ty) = - TypedExpression - { _typedType = ty, - _typedExpression = ExpressionIden (IdenVar v) + TypedIden + { _typedIdenType = ty, + _typedIden = IdenVar v } applyCoercions :: @@ -133,10 +133,20 @@ applyCoercion :: Expression -> Sem r Expression applyCoercion loc (CoercionInfo {..}, subs) e = do - e' <- expandArity loc (subsIToE subs) _coercionInfoArgs _coercionInfoResult + e' <- expandArity' loc (subsIToE subs) _coercionInfoArgs _coercionInfoResult return $ ExpressionApplication (Application e' e ImplicitInstance) +expandArity' :: + (Members '[Error TypeCheckerError, NameIdGen] r) => + Interval -> + Subs -> + [FunctionParameter] -> + Iden -> + Sem r Expression +expandArity' loc subs params iden = + expandArity loc subs params (ExpressionIden (set (idenName . nameLoc) loc iden)) + expandArity :: (Members '[Error TypeCheckerError, NameIdGen] r) => Interval -> diff --git a/src/Juvix/Compiler/Store/Internal/Data/CoercionInfo.hs b/src/Juvix/Compiler/Store/Internal/Data/CoercionInfo.hs index aed817953..e0e9081e0 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/CoercionInfo.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/CoercionInfo.hs @@ -10,7 +10,7 @@ data CoercionInfo = CoercionInfo { _coercionInfoInductive :: Name, _coercionInfoParams :: [InstanceParam], _coercionInfoTarget :: InstanceApp, - _coercionInfoResult :: Expression, + _coercionInfoResult :: Iden, _coercionInfoArgs :: [FunctionParameter] } deriving stock (Eq, Generic) diff --git a/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs b/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs index e3065f573..edf6b75a7 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs @@ -44,7 +44,7 @@ instance NFData InstanceFun data InstanceInfo = InstanceInfo { _instanceInfoInductive :: InductiveName, _instanceInfoParams :: [InstanceParam], - _instanceInfoResult :: Expression, + _instanceInfoResult :: Iden, _instanceInfoArgs :: [FunctionParameter] } deriving stock (Eq, Generic)