Re: [GHC] #11171: the 'impossible' happened when messing with existenial quantification and typed holes

6 Dec 2015

      #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