Skip to content

Commit 265db69

Browse files
committed
Dereference metavariables in types before structural inspections
1 parent b4b9974 commit 265db69

File tree

1 file changed

+9
-4
lines changed

1 file changed

+9
-4
lines changed

src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
{-# LANGUAGE RankNTypes, CPP, TupleSections #-}
1+
{-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-}
22
module GF.Compile.TypeCheck.ConcreteNew( checkLType, checkLType', inferLType, inferLType' ) where
33

44
-- The code here is based on the paper:
@@ -943,6 +943,10 @@ instantiate scope t (VProd Implicit x ty1 ty2) = do
943943
VClosure env ty2 -> eval ((x,tnk):env) ty2 []
944944
ty2 -> return ty2
945945
instantiate scope (App t (ImplArg (Meta i))) ty2
946+
instantiate scope t ty@(VMeta thk args) = getRef thk >>= \case
947+
Evaluated _ v -> instantiate scope t v
948+
Residuation _ _ (Just v) -> instantiate scope t v
949+
_ -> return (t,ty) -- We don't have enough information to try any instantiation
946950
instantiate scope t ty = do
947951
return (t,ty)
948952

@@ -1121,9 +1125,10 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go ty acc) [] sc_tys
11211125
| m `elem` acc = return acc
11221126
| otherwise = do res <- getRef m
11231127
case res of
1124-
Evaluated _ v -> go v acc
1125-
Residuation _ _ Nothing -> foldM follow (m:acc) args
1126-
_ -> return acc
1128+
Evaluated _ v -> go v acc
1129+
Residuation _ _ Nothing -> foldM follow (m:acc) args
1130+
Residuation _ _ (Just v) -> go v acc
1131+
_ -> return acc
11271132
go (VApp f args) acc = foldM follow acc args
11281133
go v acc = unimplemented ("go "++showValue v)
11291134

0 commit comments

Comments
 (0)