Fix #12430 by expanding type synonyms in injTyVarsOfType
authorRyan Scott <ryan.gl.scott@gmail.com>
Mon, 15 Oct 2018 17:48:21 +0000 (13:48 -0400)
committerBen Gamari <ben@smart-cactus.org>
Mon, 15 Oct 2018 21:59:20 +0000 (17:59 -0400)
We weren't expanding type synonyms when determining the
injective type variables of a type, leading to certain non-injective
families being mistakenly labeled as injective (#12430). Easily fixed
with a tactical use of `coreView`.

Test Plan: make test TEST=T12430

Reviewers: bgamari, goldfire

Reviewed By: goldfire

Subscribers: goldfire, rwbarton, carter

GHC Trac Issues: #12430

Differential Revision: https://phabricator.haskell.org/D5228

compiler/typecheck/FamInst.hs
testsuite/tests/typecheck/should_fail/T12430.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T12430.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/all.T

index dc6eab8..8f1f7ba 100644 (file)
@@ -792,6 +792,9 @@ injTyVarsOfType :: TcTauType -> TcTyVarSet
 -- E.g.   Suppose F is injective in its second arg, but not its first
 --        then injVarOfType (Either a (F [b] (a,c))) = {a,c}
 --        Determining the overall type determines a,c but not b.
+injTyVarsOfType ty
+  | Just ty' <- coreView ty -- #12430
+  = injTyVarsOfType ty'
 injTyVarsOfType (TyVarTy v)
   = unitVarSet v `unionVarSet` injTyVarsOfType (tyVarKind v)
 injTyVarsOfType (TyConApp tc tys)
diff --git a/testsuite/tests/typecheck/should_fail/T12430.hs b/testsuite/tests/typecheck/should_fail/T12430.hs
new file mode 100644 (file)
index 0000000..03cded2
--- /dev/null
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeFamilyDependencies #-}
+module T12430 where
+
+type C a = Int
+type family F x = y | y -> x where
+  F x = C x
diff --git a/testsuite/tests/typecheck/should_fail/T12430.stderr b/testsuite/tests/typecheck/should_fail/T12430.stderr
new file mode 100644 (file)
index 0000000..c3d9446
--- /dev/null
@@ -0,0 +1,8 @@
+
+T12430.hs:6:3: error:
+    • Type family equation violates injectivity annotation.
+      Type variable ‘x’ cannot be inferred from the right-hand side.
+      In the type family equation:
+        F x = C x -- Defined at T12430.hs:6:3
+    • In the equations for closed type family ‘F’
+      In the type family declaration for ‘F’
index 274dcc6..501c5e1 100644 (file)
@@ -413,6 +413,7 @@ test('T12177', normal, compile_fail, [''])
 test('T12406', normal, compile_fail, [''])
 test('T12170a', normal, compile_fail, [''])
 test('T12124', normal, compile_fail, [''])
+test('T12430', normal, compile_fail, [''])
 test('T12589', normal, compile_fail, [''])
 test('T12529', normal, compile_fail, [''])
 test('T12563', normal, compile_fail, [''])