Opened 5 months ago

Last modified 7 weeks ago

## #15561 new bug

# TypeInType: Type error conditioned on ordering of GADT and type family definitions

Reported by: | Bj0rn | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.6.1 |

Component: | Compiler | Version: | 8.4.3 |

Keywords: | TypeInType, TypeFamilies, GADTs | Cc: | |

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

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

Blocked By: | Blocking: | ||

Related Tickets: | #12088, #12643, #14668, #15987 | Differential Rev(s): | |

Wiki Page: |

### Description

Consider this code which successfully compiles:

{-# LANGUAGE TypeInType, TypeFamilies, GADTs #-} module Bug where class HasIndex a where type Index a emptyIndex :: IndexWrapper a instance HasIndex [a] where type Index [a] = Int emptyIndex = Wrap 0 data IndexWrapper a where Wrap :: Index a -> IndexWrapper a type family UnwrapAnyWrapperLikeThing (a :: t) :: k type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a

The mere act of moving the definition of `IndexWrapper`

anywhere below the definition of `UnwrapAnyWrapperLikeThing`

makes the type family instance at the bottom of the example fail compilation, with this error:

Bug.hs:17:15: error: • Illegal type synonym family application in instance: Index [b] • In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’ | 17 | type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.

The problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing`

in this example) in module `A`

and all of the other definitions in module `B`

that imports `A`

.

Ideally, I would have liked to add a `HasIndex a`

constraint to the `Wrap`

constructor, but that disqualifies use of `'Wrap`

on the type level. This does make me feel like I'm on shaky ground to begin with.

I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.

### Change History (3)

### comment:1 Changed 5 months ago by

### comment:2 Changed 5 months ago by

Yes, I think it's #12088 again. Here is what I think is going on.

- The declaration
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a

mentions

`IndexWrapper`

, so the latter must be typechecked first (and it is).

`IndexWrapper`

is mutually recursive with`HasIndex`

and`Index`

, so they must be typechecked together (and they are).

- Returning to
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a

we can see that

`a :: Index [b]`

. Now, if we have already processedinstance HasIndex [a] where type Index [a] = Int

then that mens

`a :: Int`

, and all is well. (This does involve some type family reduction in the patterns of a`type instance`

. Where does that happen?)

- But if we have not yet processed the instance for
`HasIndex`

then we complain that the LHStype instance UnwrapAnyWrapperLikeThing ('Wrap (a :: Index [b]) :: IndexWrapper [b]) = a

mentions

`Index [b]`

on the LHS.

For now, a robust solution is to force GHC to deal with the instance of `HasIndex`

first,(mis)-using a Template Haskell splice. For example, this compiles fine, but fails if you remove the splice

type family UnwrapAnyWrapperLikeThing (a :: t) :: k class HasIndex a where type Index a emptyIndex :: IndexWrapper a data IndexWrapper a where Wrap :: Index a -> IndexWrapper a instance HasIndex [a] where type Index [a] = Int emptyIndex = Wrap 0 $([d| |]) -- Empty Template Haskell top level splice type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a

More grist for the #12088 mill!

### comment:3 Changed 7 weeks ago by

Related Tickets: | → #12088, #12643, #14668, #15987 |
---|

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

Perhaps related to #12088 and https://ghc.haskell.org/trac/ghc/wiki/InterleavingTypeInstanceChecking