From 8c90e6c758769b068aea2891b26cc17577b6d36a Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Mon, 12 Apr 2021 14:46:30 -0400 Subject: Fix #19682 by breaking cycles in Deriveds This commit expands the old Note [Type variable cycles in Givens] to apply as well to Deriveds. See the Note for details and examples. This fixes a regression introduced by my earlier commit that killed off the flattener in favor of the rewriter. A few other things happened along the way: * unifyTest was renamed to touchabilityTest, because that's what it does. * isInsolubleOccursCheck was folded into checkTypeEq, which does much of the same work. To get this to work out, though, we need to keep more careful track of what errors we spot in checkTypeEq, and so CheckTyEqResult has become rather more glorious. * A redundant Note or two was eliminated. * Kill off occCheckForErrors; due to Note [Rewriting synonyms], the extra occCheckExpand here is always redundant. * Store blocked equalities separately from other inerts; less stuff to look through when kicking out. Close #19682. test case: typecheck/should_compile/T19682{,b} --- testsuite/tests/dependent/should_fail/T15859a.stderr | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'testsuite/tests/dependent') diff --git a/testsuite/tests/dependent/should_fail/T15859a.stderr b/testsuite/tests/dependent/should_fail/T15859a.stderr index 1fdac765f2..491733c7b9 100644 --- a/testsuite/tests/dependent/should_fail/T15859a.stderr +++ b/testsuite/tests/dependent/should_fail/T15859a.stderr @@ -1,6 +1,8 @@ -T15859a.hs:19:5: error: - • Cannot apply expression of type ‘KindOf A’ - to a visible type argument ‘Int’ - • In the expression: (undefined :: KindOf A) @Int - In an equation for ‘a’: a = (undefined :: KindOf A) @Int +T15859a.hs:19:26: error: + • Expected kind ‘k0’, but ‘A’ has kind ‘forall k -> k -> *’ + Cannot instantiate unification variable ‘k0’ + with a kind involving polytypes: forall k -> k -> * + • In the first argument of ‘KindOf’, namely ‘A’ + In an expression type signature: KindOf A + In the expression: undefined :: KindOf A -- cgit v1.2.1