Commit d0716279 authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

Fix #17067 by making data family type constructors actually injective

`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.
parent 1230d6f9
Pipeline #9510 passed with stages
in 338 minutes and 25 seconds
......@@ -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
......
{-# 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
......@@ -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, [''])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment