Typechecker allows a skolem to escapt
This program make GHC 7.4 and GHC 7.6 rc1 give a Lint error, because a skolem is allowed to escape
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, FlexibleContexts #-}
module Foo where
type family F a
class C b where {}
foo :: a -> F a
foo x = error "urk"
h :: (b -> ()) -> Int
h = error "urk"
f = h (\x -> let g :: C (F a) => a -> Int
g y = length [x, foo y]
in ())
This is the result with 7.6 rc1
*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: Warning:
In the expression: Foo.h @ (Foo.F a_o) (\ _ -> GHC.Tuple.())
@ a_o is out of scope
*** Offending Program ***
Foo.h :: forall b_aeJ. (b_aeJ -> ()) -> GHC.Types.Int
[LclIdX]
Foo.h =
\ (@ b_d) ->
GHC.Err.error
@ ((b_d -> ()) -> GHC.Types.Int) (GHC.CString.unpackCString# "urk")
Foo.f :: GHC.Types.Int
[LclIdX]
Foo.f = Foo.h @ (Foo.F a_o) (\ _ -> GHC.Tuple.())
Foo.foo :: forall a_aeL. a_aeL -> Foo.F a_aeL
[LclIdX]
Foo.foo =
\ (@ a_g) _ ->
GHC.Err.error @ (Foo.F a_g) (GHC.CString.unpackCString# "urk")
*** End of Offense ***
Trac metadata
Trac field | Value |
---|---|
Version | 7.4.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |