[GHC] #7861: deferred type error with rankNTypes

[GHC]

#7861: deferred type error with rankNTypes
-------------------------------+--------------------------------------------
    Reporter:  guest           |       Owner:                    
        Type:  bug             |      Status:  new               
    Priority:  normal          |   Milestone:                    
   Component:  Compiler        |     Version:  7.6.2             
    Keywords:                  |          Os:  Linux             
Architecture:  x86_64 (amd64)  |     Failure:  Compile-time crash
  Difficulty:  Unknown         |    Testcase:                    
   Blockedby:                  |    Blocking:                    
     Related:                  |  
-------------------------------+--------------------------------------------
Changes (by simonpj):

  * difficulty:  => Unknown


Old description:

> {-# LANGUAGE RankNTypes #-}
>
> type A a = forall b. (a -> b) -> b
>
> doA :: (a -> b) -> A a -> b
> doA f l = l f
>
> -- f :: A a -> [a] -> [a]   -- correct type
> f :: A a -> a               -- wrong type
> f = doA (:)
>
> main = return ()
>
> -- compiled with wrong type and -fdefer-type-errors
> -- gives ghc panic
> -- F.hs:10:5: Warning:
> --     Occurs check: cannot construct the infinite type: a0 = [a0] ->
> [a0]
> --     Expected type: A a -> a
> --       Actual type: A a0 -> a
> --     In the return type of a call of `doA'
> --     In the expression: doA (:)
> --     In an equation for `f': f = doA (:)
> --
> -- F.hs:10:9: Warning:
> --     Couldn't match type `a' with `[a0] -> [a0]'
> --       `a' is a rigid type variable bound by
> --           the type signature for f :: A a -> a at F.hs:9:6
> --     Expected type: a0 -> a
> --       Actual type: a0 -> [a0] -> [a0]
> --     In the first argument of `doA', namely `(:)'
> --     In the expression: doA (:)
> --     In an equation for `f': f = doA (:)
> -- ghc: panic! (the 'impossible' happened)
> --   (GHC version 7.6.2 for x86_64-unknown-linux):
> --      evTermCoercion
> --     error @ghc-prim:GHC.Prim.Any{(w) tc 31N}
> --              ghc-prim:GHC.Prim.*{(w) tc 34d}
> --            ghc-prim:GHC.Types.~{(w) tc 31Q} ([ghc-
> prim:GHC.Prim.Any{(w) tc 31N}
> --                                                 ghc-
> prim:GHC.Prim.*{(w) tc 34d}]
> --                                              -> [ghc-
> prim:GHC.Prim.Any{(w) tc 31N}
> --                                                    ghc-
> prim:GHC.Prim.*{(w) tc 34d}])
> --           F.hs:10:5:
> --     Occurs check: cannot construct the infinite type: a0 = [a0] ->
> [a0]
> --     Expected type: A a -> a
> --       Actual type: A a0 -> a
> --     In the return type of a call of `doA'
> --     In the expression: doA (:)
> --     In an equation for `f': f = doA (:)
> -- (deferred type error)

New description:

 {{{
 {-# LANGUAGE RankNTypes #-}

 type A a = forall b. (a -> b) -> b

 doA :: (a -> b) -> A a -> b
 doA f l = l f

 -- f :: A a -> [a] -> [a]   -- correct type
 f :: A a -> a               -- wrong type
 f = doA (:)

 main = return ()
 }}}
 compiled with wrong type and `-fdefer-type-errors`
 gives ghc panic
 {{{
 -- F.hs:10:5: Warning:
 --     Occurs check: cannot construct the infinite type: a0 = [a0] -> [a0]
 --     Expected type: A a -> a
 --       Actual type: A a0 -> a
 --     In the return type of a call of `doA'
 --     In the expression: doA (:)
 --     In an equation for `f': f = doA (:)
 --
 -- F.hs:10:9: Warning:
 --     Couldn't match type `a' with `[a0] -> [a0]'
 --       `a' is a rigid type variable bound by
 --           the type signature for f :: A a -> a at F.hs:9:6
 --     Expected type: a0 -> a
 --       Actual type: a0 -> [a0] -> [a0]
 --     In the first argument of `doA', namely `(:)'
 --     In the expression: doA (:)
 --     In an equation for `f': f = doA (:)
 -- ghc: panic! (the 'impossible' happened)
 --   (GHC version 7.6.2 for x86_64-unknown-linux):
 --      evTermCoercion
 --     error @ghc-prim:GHC.Prim.Any{(w) tc 31N}
 --              ghc-prim:GHC.Prim.*{(w) tc 34d}
 --            ghc-prim:GHC.Types.~{(w) tc 31Q} ([ghc-prim:GHC.Prim.Any{(w)
 tc 31N}
 --                                                 ghc-prim:GHC.Prim.*{(w)
 tc 34d}]
 --                                              -> [ghc-
 prim:GHC.Prim.Any{(w) tc 31N}
 --                                                    ghc-
 prim:GHC.Prim.*{(w) tc 34d}])
 --           F.hs:10:5:
 --     Occurs check: cannot construct the infinite type: a0 = [a0] -> [a0]
 --     Expected type: A a -> a
 --       Actual type: A a0 -> a
 --     In the return type of a call of `doA'
 --     In the expression: doA (:)
 --     In an equation for `f': f = doA (:)
 -- (deferred type error)
 }}}

--

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7861#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler