id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
7194,Typechecker allows a skolem to escapt,simonpj,,"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 ***
}}}
",bug,closed,normal,,Compiler,7.4.2,fixed,,,Unknown/Multiple,Unknown/Multiple,None/Unknown,Unknown,T7194,,,
