#11171: the 'impossible' happened when messing with existenial quantification and typed holes -------------------------------------+------------------------------------- Reporter: TheKing42 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: duplicate | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: Compile-time | (amd64) crash | Test Case: Blocked By: | Blocking: Related Tickets: #10615 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * status: new => closed * resolution: => duplicate * related: => #10615 Comment: I can reproduce this on 7.10.2 but not on HEAD. I've pasted the actual errors I get on HEAD below, I think the panic was due to the wildcard. {{{ [1 of 1] Compiling Main ( test.lhs, interpreted ) test.lhs:13:31: error: • Found type wildcard ‘_’ standing for ‘f (Maybe (CoInd f))’ Where: ‘f’ is a rigid type variable bound by the type signature for: wrap :: Functor f => f (CoInd f) -> CoInd f at test.lhs:11:11 To use the inferred type, enable PartialTypeSignatures • In the type signature for: igo :: Maybe (CoInd f) -> _ In an equation for ‘wrap’: 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 • Relevant bindings include fc :: f (CoInd f) (bound at test.lhs:12:8) wrap :: f (CoInd f) -> CoInd f (bound at test.lhs:12:3) test.lhs:14:5: error: • No instance for (Functor f) • When checking that ‘igo’ has the inferred type igo :: forall (f :: * -> *). Maybe (CoInd f) -> f1 (Maybe (CoInd f1)) Probable cause: the inferred type is ambiguous In an equation for ‘wrap’: 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 test.lhs:15:42: error: • Couldn't match type ‘f1’ with ‘f’ ‘f1’ is untouchable inside the constraints: () bound by a pattern with constructor: Coinduction :: forall (f :: * -> *) r. (r -> f r) -> r -> CoInd f, in an equation for ‘igo’ at test.lhs:15:16-36 ‘f1’ is a rigid type variable bound by the inferred type of igo :: Functor f1 => Maybe (CoInd f1) -> f (Maybe (CoInd f)) at test.lhs:13:12 ‘f’ is a rigid type variable bound by the type signature for: wrap :: Functor f => f (CoInd f) -> CoInd f at test.lhs:11:11 Possible fix: add a type signature for ‘igo’ Expected type: f (Maybe (CoInd f)) Actual type: f1 (Maybe (CoInd f1)) • In the expression: fmap (Just . Coinduction step) $ step seed In an equation for ‘igo’: igo (Just (Coinduction step seed)) = fmap (Just . Coinduction step) $ step seed In an equation for ‘wrap’: 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 • Relevant bindings include step :: r -> f1 r (bound at test.lhs:15:28) igo :: Maybe (CoInd f1) -> f (Maybe (CoInd f)) (bound at test.lhs:14:5) fc :: f (CoInd f) (bound at test.lhs:12:8) wrap :: f (CoInd f) -> CoInd f (bound at test.lhs:12:3) test.lhs:23:12: error: • Could not deduce (Functor f1) arising from a use of ‘fmap’ from the context: Functor f bound by the type signature for: cowrap :: Functor f => Ind f -> f (Ind f) at test.lhs:20:13-45 Possible fix: add (Functor f1) to the context of the type signature for: igo :: f1 (f1 (Ind f1)) -> f1 (Ind f1) • In the expression: fmap (\ fInd -> Ind $ \ fold -> fold $ fmap (( \ x_ -> flipinduct x_ fold)) fInd) In an equation for ‘igo’: igo = fmap (\ fInd -> Ind $ \ fold -> fold $ fmap (( \ x_ -> flipinduct x_ fold)) fInd) In an equation for ‘cowrap’: cowrap = induction igo where igo :: f (f (Ind f)) -> f (Ind f) igo = fmap (\ fInd -> Ind $ \ fold -> ...) test.lhs:23:49: error: • Could not deduce (Functor f1) arising from a use of ‘fmap’ from the context: Functor f bound by the type signature for: cowrap :: Functor f => Ind f -> f (Ind f) at test.lhs:20:13-45 Possible fix: add (Functor f1) to the context of a type expected by the context: (f1 r -> r) -> r or the type signature for: igo :: f1 (f1 (Ind f1)) -> f1 (Ind f1) • In the second argument of ‘($)’, namely ‘fmap (( \ x_ -> flipinduct x_ fold)) fInd’ In the expression: fold $ fmap (( \ x_ -> flipinduct x_ fold)) fInd In the second argument of ‘($)’, namely ‘\ fold -> fold $ fmap (( \ x_ -> flipinduct x_ fold)) fInd’ Failed, modules loaded: none. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11171#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11171: the 'impossible' happened when messing with existenial quantification and typed holes -------------------------------------+------------------------------------- Reporter: TheKing42 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: duplicate | Keywords: Operating System: Linux | Architecture: x86_64 Type of failure: Compile-time | (amd64) crash | Test Case: Blocked By: | Blocking: Related Tickets: #10615 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I fixed a bunch of wildcard-related stuff recently. So can you try with HEAD (or 8.0 when it comes) and say if you still think there's a problem? Thanks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11171#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler