the 'impossible' happened when messing with existenial quantification and typed holes

First of all, I am quite honored that I was able to do something that GHC considered impossible. (Funny too. Just the other day, I was trying to break GHC and failed. Today, I was doing something I thought was rather mundane (although it was acting somewhat funky anyway)). Anyway, here is my error message:

*Main> :r
[1 of 1] Compiling Main             ( pad.lhs, interpreted )

pad.lhs:12:25:
    Couldn't match type ‘f1’ with ‘f’
      ‘f1’ is a rigid type variable bound by
           the type signature for
             wrap :: Functor f1 => f1 (CoInd f1) -> CoInd f1
           at pad.lhs:11:11ghc: panic! (the 'impossible' happened)
  (GHC version 7.10.2 for x86_64-unknown-linux):
        No skolem info: f_abyA[sk]

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

And here is the code

> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-}

> newtype Ind f = Ind {flipinduct :: forall r. (f r -> r) -> r}
> induction = flip flipinduct

> data CoInd f = forall r. Coinduction (r -> f r) r
> coinduction = Coinduction

> data StringF rec = Nil | Cons Char rec deriving Functor

> wrap :: (Functor f) => f (CoInd f) -> CoInd f
> wrap fc = coinduction igo Nothing where
>   igo :: Maybe (CoInd f) -> _
>   igo Nothing  = fmap Just fc
>   igo (Just (Coinduction step seed)) = fmap (Just . Coinduction step) $ step seed

> convert :: (Functor f) => Ind f -> CoInd f
> convert = induction wrap

> cowrap :: (Functor f) => Ind f -> f (Ind f)
> cowrap = induction igo where
>    igo :: f (f (Ind f)) -> f (Ind f)
>    igo = fmap (\fInd -> Ind $ \fold -> fold $ fmap (`flipinduct` fold) fInd)

> convert' :: (Functor f) => Ind f -> CoInd f
> convert' = coinduction cowrap

I think the important parts are only "CoInd", "wrap", and "igo", but I included it all just to be sure (and I'm lazy).

Trac metadata

Trac field	Value
Version	7.10.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture