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 |