Opened 4 months ago

Last modified 2 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:2 Changed 4 months ago by simonpj

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 processed

instance 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 LHS
    type 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 2 weeks ago by RyanGlScott

Note: See TracTickets for help on using tickets.