@@ -379,9 +379,10 @@ unify ctxt env topx topy dont holes =
379379 unArgs vs xs ys
380380
381381 metavarApp tm = let (f, args) = unApply tm in
382− metavar f &&
383− all (\x -> metavarApp x) args
384− && nub args == args
382+ (metavar f &&
383+ all (\x -> metavarApp x) args
384+ && nub args == args) ||
385+ globmetavar tm
385386 metavarArgs tm = let (f, args) = unApply tm in
386387 all (\x -> metavar x || inenv x) args
387388 && nub args == args
@@ -413,14 +414,22 @@ unify ctxt env topx topy dont holes =
413414
414415 rigid (P (DCon _ _) _ _) = True
415416 rigid (P (TCon _ _) _ _) = True
416− rigid t@(P Ref _ _) = inenv t
417+ rigid t@(P Ref _ _) = inenv t || globmetavar t
417418 rigid (Constant _) = True
418419 rigid (App f a) = rigid f && rigid a
419− rigid t = not (metavar t)
420+ rigid t = not (metavar t) || globmetavar t
421+
422+ globmetavar t = case unApply t of
423+ (P _ x _, _) ->
424+ case lookupDef x ctxt of
425+ [TyDecl _ _] -> True
426+ _ -> False
427+ _ -> False
420428
421429 metavar t = case t of
422− P _ x _ -> (x `elem` holes || holeIn env x) &&
423− not (x `elem` dont)
430+ P _ x _ -> ((x `elem` holes || holeIn env x) &&
431+ not (x `elem` dont))
432+ || globmetavar t
424433 _ -> False
425434 pat t = case t of
426435 P _ x _ -> x `elem` holes || patIn env x