Fix #17067 by making data family type constructors actually injective
authorRyan Scott <ryan.gl.scott@gmail.com>
Sat, 17 Aug 2019 12:27:35 +0000 (08:27 -0400)
committerMarge Bot <ben+marge-bot@smart-cactus.org>
Sun, 18 Aug 2019 09:18:01 +0000 (05:18 -0400)
`TcTyClsDecls.tcFamDecl1` was using `NotInjective` when creating data
family type constructors, which is just plain wrong. This tweaks it
to use `Injective` instead.

Fixes #17067.

compiler/typecheck/TcTyClsDecls.hs
testsuite/tests/typecheck/should_compile/T17067.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index b9e51fa..91536e5 100644 (file)
@@ -1938,11 +1938,12 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
   ; let (_, final_res_kind) = splitPiTys res_kind
   ; checkDataKindSig DataFamilySort final_res_kind
   ; tc_rep_name <- newTyConRepName tc_name
-  ; let tycon = mkFamilyTyCon tc_name binders
+  ; let inj   = Injective $ replicate (length binders) True
+        tycon = mkFamilyTyCon tc_name binders
                               res_kind
                               (resultVariableName sig)
                               (DataFamilyTyCon tc_rep_name)
-                              parent NotInjective
+                              parent inj
   ; return tycon }
 
   | OpenTypeFamily <- fam_info
diff --git a/testsuite/tests/typecheck/should_compile/T17067.hs b/testsuite/tests/typecheck/should_compile/T17067.hs
new file mode 100644 (file)
index 0000000..2666c4c
--- /dev/null
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+module T17067 where
+
+import Data.Kind
+
+data family D1 a
+data family D2 :: Type -> Type
+
+type family F a
+type instance F (D1 a) = a
+type instance F (D2 a) = a
index e393fe4..9a91f4e 100644 (file)
@@ -686,3 +686,4 @@ test('UnliftedNewtypesDifficultUnification', normal, compile, [''])
 test('T16832', normal, ghci_script, ['T16832.script'])
 test('T16946', normal, compile, [''])
 test('T17007', normal, compile, [''])
+test('T17067', normal, compile, [''])