Opened 3 days ago

Last modified 3 days ago

#15740 new bug

Type family with higher-rank result is too accepting

Reported by: goldfire Owned by:
Priority: highest Milestone: 8.8.1
Component: Compiler Version: 8.6.1
Keywords: TypeFamilies, TypeInType Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

GHC accepts this garbage:

type family F2 :: forall k. k -> Type
data SBool :: Bool -> Type
data Nat
data SNat :: Nat -> Type
type instance F2 = SBool
type instance F2 = SNat

The family F2 should have an arity of 0, meaning that only one instance is possible -- and the RHS of that instance must have kind forall k. k -> Type. In other words, even accepting only one of the instances above is hogwash.

This is from comment:15:ticket:11719, but you don't have to read that to understand this.

Change History (4)

comment:1 Changed 3 days ago by RyanGlScott

Cc: RyanGlScott added

comment:2 Changed 3 days ago by RyanGlScott

As noted in comment:16:ticket:11719, this behavior is a regression from GHC 8.2, which rejects those instances. The first commit to demonstrate this behavior is 4239238306e911803bf61fdda3ad356fd0b42e05 (Fix #12369 by being more flexible with data insts).

comment:3 Changed 3 days ago by simonpj

Milestone: 8.8.1
Priority: normalhigh

Let's make sure this is fixed in 8.8. Can't be too hard, hence making high priority...

Last edited 3 days ago by simonpj (previous) (diff)

comment:4 Changed 3 days ago by simonpj

Priority: highhighest
Note: See TracTickets for help on using tickets.