Opened 3 years ago

Closed 3 years ago

## #9144 closed bug (fixed)

# Incorrect error reported with poly-kinded type families

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

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 7.8.2 |

Keywords: | Cc: | ||

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

Type of failure: | None/Unknown | Test Case: | polykinds/T9144 |

Blocked By: | Blocking: | ||

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

Wiki Page: |

### Description (last modified by )

When I compile

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs, RankNTypes #-} module Bug where import Data.Proxy import GHC.TypeLits data family Sing (a :: k) data SomeSing :: KProxy k -> * where SomeSing :: forall (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k) class kproxy ~ 'KProxy => SingKind (kproxy :: KProxy k) where fromSing :: forall (a :: k). Sing a -> DemoteRep ('KProxy :: KProxy k) toSing :: DemoteRep ('KProxy :: KProxy k) -> SomeSing ('KProxy :: KProxy k) type family DemoteRep (kproxy :: KProxy k) :: * data Foo = Bar Nat data FooTerm = BarTerm Integer data instance Sing (x :: Foo) where SBar :: Sing n -> Sing (Bar n) type instance DemoteRep ('KProxy :: KProxy Nat) = Integer type instance DemoteRep ('KProxy :: KProxy Foo) = FooTerm instance SingKind ('KProxy :: KProxy Nat) where fromSing = undefined toSing = undefined instance SingKind ('KProxy :: KProxy Foo) where fromSing (SBar n) = BarTerm (fromSing n) toSing n = case toSing n of SomeSing n' -> SomeSing (SBar n')

I get (with `-fprint-explicit-kinds`

)

/Users/rae/temp/Bug.hs:33:32: Couldn't match type ‘FooTerm’ with ‘Integer’ Expected type: Integer Actual type: DemoteRep Nat ('KProxy Nat) In the first argument of ‘BarTerm’, namely ‘(fromSing n)’ In the expression: BarTerm (fromSing n) /Users/rae/temp/Bug.hs:34:26: Couldn't match type ‘Integer’ with ‘FooTerm’ Expected type: DemoteRep Nat ('KProxy Nat) Actual type: DemoteRep Foo ('KProxy Foo) In the first argument of ‘toSing’, namely ‘n’ In the expression: toSing n

The second error reported is correct -- the last line in the code should start `toSing (BarTerm n) = ...`

to fix the code. However, the first error reported is bogus, given that `DemoteRep ('KProxy :: KProxy Nat)`

is clearly `Integer`

.

I tried to simplify the test case with no luck -- sorry.

### Change History (4)

### comment:1 Changed 3 years ago by

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

### comment:2 Changed 3 years ago by

Happily, I believe that this works on the 7.8 branch, and HEAD, and hence is already fixed. I don't know what the fix was! Still pending: add the test case to HEAD

Simon

### comment:4 Changed 3 years ago by

Resolution: | → fixed |
---|---|

Status: | new → closed |

Test Case: | → polykinds/T9144 |

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

Corrected typo in initial report (

`FooTerm`

-->`BarTerm`

in a critical spot).