Opened 21 months ago

Closed 7 months ago

## #12176 closed bug (fixed)

# Failure of bidirectional type inference at the kind level

Reported by: | goldfire | Owned by: | goldfire |
---|---|---|---|

Priority: | normal | Milestone: | 8.4.1 |

Component: | Compiler | Version: | 8.0.1 |

Keywords: | TypeInType | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | dependent/should_compile/T12176 |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description (last modified by )

I'm feeling particularly sadistic towards GHC at the moment, and so I fed it this:

import Data.Kind data Proxy :: forall k. k -> Type where MkProxy :: forall k (a :: k). Proxy a data X where MkX :: forall (k :: Type) (a :: k). Proxy a -> X type Expr = (MkX :: forall (a :: Bool). Proxy a -> X) type family Foo (x :: forall (a :: k). Proxy a -> X) where Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)

Incredibly, GHC accepts it! And it even means what I wish it to, with GHCi telling me the following (with `-fprint-explicit-kinds`

):

λ> :i Foo type family Foo k (x :: forall (a :: k). Proxy k a -> X) :: Proxy * k where [k] Foo k ('MkX k) = 'MkProxy * k

That is, I wished to extract the kind parameter to `MkK`

, matching against a partially-applied `MkX`

, and GHC understood that intention.

However, sadly, writing `Foo Expr`

produces

• Expected kind ‘forall (a :: k0). Proxy k0 a -> X’, but ‘Expr a0’ has kind ‘Proxy Bool a0 -> X’ • In the first argument of ‘Foo’, namely ‘Expr’ In the type ‘Foo Expr’ In the type family declaration for ‘XXX’

For some reason, `Expr`

is getting instantiated when it shouldn't be.

Perhaps there's a simpler test case demonstrating the bug, but I feel so gleeful that this chicanery is accepted at all that I wanted to post.

### Change History (3)

### comment:1 Changed 7 months ago by

### comment:2 Changed 7 months ago by

Status: | new → merge |
---|---|

Test Case: | → dependent/should_compile/T12176 |

Merge if convenient, but I don't think this one ruins anyone's day.

### comment:3 Changed 7 months ago by

Description: | modified (diff) |
---|---|

Milestone: | → 8.4.1 |

Resolution: | → fixed |

Status: | merge → closed |

Given that this isn't a regression of 8.2 I'm going to punt this off until 8.4.1 unless someone objects.

**Note:**See TracTickets for help on using tickets.

In 1696dbf/ghc: