#9636: Function with type error accepted -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:13 rwbarton]:
Anyways, failure of what I have learned is called "the substitution lemma" is far more unintuitive to me
If the substitution lemma doesn't hold, then (perhaps) FC, and by extension Haskell, is no longer type-safe. In other words, I don't believe that the type system is capable of ruling out `T Bool`, without major surgery. So, maybe we can report errors to the user if we see `T Bool` in source code, but if `T Bool` ends up sloshing around internally, GHC will respect it as a valid type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9636#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler