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?!? >_<

You should post at least some code. As far as I know, type-level programs are best debugged with :kind!, holes and Any as type-level hole. — András Kovács
The code I have is large and complicated, and I doubt anybody will be able to follow it. What I'm asking for is tips on how to hunt down where the problem is, so I know where to start looking. — MathematicalOrchid
This comment is just to potentially enable me to say 'called it!' later: are you assuming some type family is injective? — Cactus
@Cactus LOL! I've got GADTs, existential quantification, rank-N types and overlapping instances... but no type families. — MathematicalOrchid

Eliza Brandt Eliza Brandt · Accepted Answer · 2018-05-23T21:29:51

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.

How to debug type-level programs

1 Answers