## #15545 closed bug (fixed)

# Forced to enable TypeInType because of (i ~ i)

Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.6.1 |

Component: | Compiler | Version: | 8.5 |

Keywords: | TypeInType | Cc: | |

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

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

Blocked By: | Blocking: | ||

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

Wiki Page: |

### Description

I don't know if this is a bug but `i ~ i`

holds by reflexivity so I would not have expected it to require `TypeInType`

$ ghci -ignore-dot-ghci GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help Prelude> :set -XPolyKinds -XGADTs Prelude> import Data.Kind Prelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a <interactive>:3:45: error: • Data constructor ‘NP’ constrains the choice of kind parameter: i ~ i Use TypeInType to allow this • In the definition of data constructor ‘NP’ In the data type declaration for ‘NP’ Prelude Data.Kind>

I would rather expect the warning I get after enabling `TypeInType`

Prelude Data.Kind> :set -XTypeInType Prelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a <interactive>:8:28: error: • Couldn't match ‘k’ with ‘i’ • In the data declaration for ‘NP’

**ps** making sure this is OK as well; it works after enabling `-XTypeInType`

and quantifying with `-XRankNTypes`

(is this using polymorphic recursion?)

Prelude Data.Kind> :set -XTypeInType -XRankNTypes Prelude Data.Kind> data NP :: forall i k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a Prelude Data.Kind> :t NP NP :: forall i (f :: i -> *) (a :: i). f a -> NP f a

it also works for

data NP :: forall k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a data NP :: forall i. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a data NP :: (k -> Type) -> forall i. (i -> Type) where NP :: f a -> NP f a

### Change History (2)

### comment:1 Changed 4 months ago by

Milestone: | → 8.6.1 |
---|---|

Related Tickets: | → #15195 |

Resolution: | → fixed |

Status: | new → closed |

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

This is a rather cheeky solution, but this problem simply doesn't exist on GHC 8.6, since

`TypeInType`

is now simply a synonym for`DataKinds`

and`PolyKinds`

, and`PolyKinds`

now grants access to all of the features that used to be exclusive to`TypeInType`

. See #15195.