Opened 3 years ago

Closed 3 years ago

## #13197 closed bug (invalid)

# Perplexing levity polymorphism issue

Reported by: | bgamari | Owned by: | |
---|---|---|---|

Priority: | highest | Milestone: | 8.2.1 |

Component: | Compiler (Type checker) | Version: | 8.1 |

Keywords: | typeable | Cc: | goldfire |

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

Type of failure: | GHC rejects valid program | Test Case: | |

Blocked By: | Blocking: | ||

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

Wiki Page: |

### Description (last modified by )

I would have expected this to compile since the levity polymorphism patch (along with Phab:D2038) was merged, but sadly it seems the typechecker isn't quite clever enough yet (or perhaps I'm the not clever one),

{-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes, TypeOperators, ViewPatterns #-} {-# LANGUAGE TypeInType #-} module Test where import Data.Kind import GHC.Exts data TypeRep (a :: k) where TypeCon :: String -> TypeRep a TypeApp :: forall k1 k2 (f :: k1 -> k2) (x :: k1). TypeRep f -> TypeRep x -> TypeRep (f x) TypeFun :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). TypeRep a -> TypeRep b -> TypeRep (a -> b) data SomeTypeRep where SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep data (a :: k1) :~~: (b :: k2) where HRefl :: a :~~: a eqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b) eqTypeRep = undefined typeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k typeRepKind = undefined toApp :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep toApp (SomeTypeRep f) (SomeTypeRep a) | TypeFun arg res <- typeRepKind f , Just HRefl <- arg `eqTypeRep` typeRepKind a = Just $ SomeTypeRep (TypeApp f a) toApp _ _ = Nothing

### Change History (4)

### comment:1 Changed 3 years ago by

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

### comment:2 Changed 3 years ago by

### comment:3 Changed 3 years ago by

This is expected behavior. Well, for me. After I've studied it and revised my expectation.

The problem is that `k2`

in the type of `TypeApp`

has kind `Type`

. But `f a`

's kind, `res`

, has type `TYPE r2`

, which we see looking at the type of `TypeFun`

. So we get a type error.

The fix is to convince GHC that `f a`

's type's kind is really `Type`

. And we can do that with one extra check:

toApp :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep toApp (SomeTypeRep f) (SomeTypeRep a) | TypeFun arg res <- typeRepKind f , Just HRefl <- arg `eqTypeRep` typeRepKind a , Just HRefl <- typeRepKind res `eqTypeRep` (undefined :: TypeRep Type) = Just $ SomeTypeRep (TypeApp f a) toApp _ _ = Nothing

This compiles for me. Note that `arg`

's kind is discovered to be `Type`

because `arg`

equals the result of a `typeRepKind`

, which always has kind `Type`

.

Fun times!

GHC should really come little trophies that you can accrue by triggering certain bizarre scenarios.

### comment:4 Changed 3 years ago by

Resolution: | → invalid |
---|---|

Status: | new → closed |

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

For the record the above fails with,