Opened 5 months ago

Closed 5 months ago

#8541 closed task (fixed)

Coercible should be higher-kinded

Reported by: nomeata Owned by: nomeata
Priority: normal Milestone:
Component: Compiler Version: 7.6.3
Keywords: Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: TcCoercible, TcCoercibleFail3 Blocked By:
Blocking: Related Tickets:

Description

Just discussed with SJP: The Coercible should be higher kinded, and it seems to be straight forward.

Given

data T f = T (f Int)
newtype List a = [a]

we want to be able to derive

Coercible (T (Either Int)) (T (Either Age))
Coercible (T List) (T [])

We now allow Coercible at a kind * -> k, with the following intuition:

  Coercible A B ⇐⇒ (forall a. Coercible (A a) (B a))

Note that this is ok independent of the role of A’s parameter, as we are not modifying that parameter here.

Allowing such constraints, we therefore, we need these constraints exist in theory (but are in fact generated on demand, so only those of the rind kindnessare visible to the constraint solver) for Either and List:

instance (Coercible a b, Coercible c d)
                           => Coercible (Either a c) (Either b d) -- old
instance Coercible a   b =>   Coercible (Either a) (Either b)     -- new
instance Coercible [a] b =>   Coercible (List a)   b              -- old
instance Coercible b   [a] => Coercible b          (List a)       -- old
instance Coercible a   b =>   Coercible (List a)   (List b)       -- old
instance Coercible []  b =>   Coercible List       b              -- new
instance Coercible b   [] =>  Coercible b          List           -- new

This solves the cases above. It does not solve all cases, though. Consider

newtype NT1 a = NT1 (a -> Int)
newtype NT2 a = NT2 (a -> Int)

and we want to solve Coercible (T NT1) (T NT2). Although, by the definition above, Coercible NT1 NT2 should hold, such a coercion cannot be created (as far as I can see).

Change History (9)

comment:1 follow-up: Changed 5 months ago by nomeata

Indeed straight forward, see 8959c69104eb032b75ec94dcf9cda3edd2b46423 (ghc) and [bbfaff2fa89b21bee058af7e6e6ddd66524524d0/testsuite]; currently on the branch wip/T8541 (I wonder why they were not auto-linked – is that only working for master?).

The code did not check saturation of type constructors, so it worked out of the box for the positive examples from here. So let’s see what happens with the negative ones...

Last edited 5 months ago by hvr (previous) (diff)

comment:2 Changed 5 months ago by nomeata

  • Status changed from new to patch
  • Test Case set to TcCoercible, TcCoercibleFail3

comment:3 in reply to: ↑ 1 Changed 5 months ago by hvr

Replying to nomeata:

currently on the branch wip/T8541 (I wonder why they were not auto-linked – is that only working for master?).

yes, it's to avoid having multiple redundant commits attached to the same ticket; so the commit will be linked to this ticket as soon as the commit becomes reachable from master for the first time.

comment:4 Changed 5 months ago by nomeata

Makes sense, given that wip/-branches can be rebased. Thanks for the clarification.

comment:5 Changed 5 months ago by goldfire

The changes certainly look sensible to me...

comment:6 Changed 5 months ago by Joachim Breitner <mail@…>

In bbfaff2fa89b21bee058af7e6e6ddd66524524d0/testsuite:

Add examples from #8541 to testsuite

comment:7 Changed 5 months ago by Joachim Breitner <mail@…>

In 90554a88bee5b492b4d4625ef30b23b9a7915347/testsuite:

Test case for undersaturated newtype in Coercions

This is related to #8541.

comment:8 Changed 5 months ago by Joachim Breitner <mail@…>

In 976a1087ae75accb4ad9d869d14641b2581c1606/ghc:

Make Coercible higher-kinded

This implements #8541. The changes are fully straight forward and work
nicely for the examples from the ticket; this is mostly due to the
existing code not checking for saturation and kindness.

comment:9 Changed 5 months ago by nomeata

  • Resolution set to fixed
  • Status changed from patch to closed

This has hit master now.

Note: See TracTickets for help on using tickets.