Opened 3 months ago

Last modified 3 months ago

#8672 new bug

:browse and roles on typefamilies

Reported by: monoidal Owned by: goldfire
Priority: low Milestone:
Component: Compiler (Type checker) Version: 7.7
Keywords: Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description

:browse on ghci tests/ghci.debugger/scripts/T8557.hs outputs a weird looking line:

type role Sing nominal
data family Sing (a :: k)
type role T8557.R:Sing[]a nominal   <--
data instance Sing a = SNil

Change History (3)

comment:1 Changed 3 months ago by simonpj

  • Owner set to goldfire

The reason this is happening is because SNil is defined, so GHC is showing the appropriate data instance. Then it tries to show the roles of the data instance, and does so badly.

Richard, two questions. First (Q1) in this case, can't the data instance have a representational role inferred? Eg this ought to work. The definition of g is currently rejected.

data family T a
data instance T [b] = MkT b

newtype Age = MkAge Int

g :: T [Age] -> T [Int]
g x = coerce x

Second question (Q2). Are role annotations allowed on data family declarations, where they could indicate which parameters are the indices:

type role T representational nominal  -- Only second param can be an index
data family T a b

data instance T a Bool = ...   -- Allowed
data instance T Bool b = ...   -- Rejected

(And similarly for type families.)

Similarly are role annotations allowed on data instance declarations, where they would be useful in exactly the same way that they are on data decls

data family T a

type role T [a] (a:nominal)
data instance T [a] = MkT a

Here we are running out of syntax! This isn't supported now because I think all parameters are automatically nominal (see Q1 for why they shouldn't be).

However, if Q1 is accepted, then :browse must have some way to display the inferred roles for a data instance, so we need syntax for that.

For now I will just suppress the display of roles for data instances.

Simon

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

comment:2 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

In 0f7381bfb382f9fd7d18ebfc1a436237e6f2e21d/ghc:

Don't print roles for data instances

See Trac #8672

comment:3 Changed 3 months ago by goldfire

I've moved the conversation about roles on data instances to #8177, where it is more relevant. Please see that ticket for further information.

Perhaps this ticket should stay open as a reminder to revisit :browse and :info if/when data instance role annotations are added.

Is there a test case?

Note: See TracTickets for help on using tickets.