How to debug type-level programs

Question

I'm trying to do some hoopy type-level programming, and it just doesn't work. I'm tearing my hair out trying to figure out why the heck GHC utterly fails to infer the type signatures I want.

Is there some way to make GHC tell me what it's doing?

I tried -ddump-tc, which just prints out the final type signatures. (Yes, they're wrong. Thanks, I already knew that.)

I also tried -ddump-tc-trace, which dumps out ~70KB of unintelligible gibberish. (In particular, I can't see any user-written identifiers mentioned anywhere.)

My code is so close to working, but somehow an extra type variable keeps appearing. For some reason, GHC can't see that this variable should be completely determined. Indeed, if I manually write the five-mile type signature, GHC happily accepts it. So I'm clearly just missing a constraint somewhere... but where?!? >_<

Answer 1

As has been mentioned in the comments, poking around with :kind and :kind! in GHCi is usually how I go about doing it, but it also surprisingly matters where you place the functions, and what looks like it should be the same, isn't always.

For instance, I was trying to make a dependently typed functor equivalent, for a personal project, which looked like

class IFunctor f where    ifmap :: (a -> b) -> f n a -> f n b  

and I was writing the instance for

data IEither a n b where    ILeft :: a -> IEither a Z b    IRight :: b -> IEither a (S n) b  

It should be fairly simple, I thought, just ignore f for the left case, apply it in the right.

I tried

instance IFunctor (IEither a) where   ifmap _ l@(ILeft _) = l    ifmap f (IRight r) = IRight $ f r 

but for the specialized version of ifmap in this case being ifmap :: (b -> c) -> IEither a Z b -> IEither a Z c, Haskell inferred the type of l to be IEither a Z b on the LHS, which, makes sense, but then refused to produce b ~ c.

So, I had to unwrap l, get the value of type a, then rewrap it to get the IEither a Z c.

This isn't just the case with dependent types, but also with rank-n types. For instance, I was trying to convert isomorphisms of a proper form into natural transformations, which should be fairly easy, I thought.

Apparently, I had to put the deconstructors in a where clause of the function, because otherwise type inference didn't work properly.