[GHC] #8137: Permited mega-polymorphic type
#8137: Permited mega-polymorphic type -------------------------------------+------------------------------------- Reporter: wvv | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.6.3 checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC accepts Architecture: Unknown/Multiple | invalid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- Mega-polymorphic type! This looks like a bug, but may be it is a feature {{{ u = u b = u 2 + u "extra" "poly" "arguments" True b' = u ++ u True eq' = (u :: Bool) == (u 3.14 :: Bool) eq'' = (u 1 :: Num t => t) == (u "strings" "a lot" :: Num z => z) eq = u == u 2 -- ghci only
:t u u :: t }}}
This code is valid for TypeChecker -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8137 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8137: Permited mega-polymorphic type ------------------------------------------------+-------------------------- Reporter: wvv | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts invalid program | Unknown/Multiple Test Case: | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: ------------------------------------------------+-------------------------- Changes (by goldfire): * status: new => closed * resolution: => invalid Comment: This is correct behavior. The definition of `u` means both that computing `u` will never terminate and that `u` has any type. The expressions that you have above will all run forever, because `u` will run forever. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8137#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8137: Permited mega-polymorphic type ------------------------------------------------+-------------------------- Reporter: wvv | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts invalid program | Unknown/Multiple Test Case: | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: ------------------------------------------------+-------------------------- Comment (by wvv): May be I misunderstood, it looks like this case is a part of 'infinite type': {{{
let u x = (x,u)
<interactive>:33:14: Occurs check: cannot construct the infinite type: t1 = t0 -> (t0, t1) In the expression: u In the expression: (x, u) In an equation for `u': u x = (x, u) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8137#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8137: Permited mega-polymorphic type ------------------------------------------------+-------------------------- Reporter: wvv | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts invalid program | Unknown/Multiple Test Case: | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: ------------------------------------------------+-------------------------- Comment (by goldfire): In the scenario in your comment above, the type `t1` must be a sub-part of the type `t1`, which is only possible with infinite types. In the original case in the bug report, we get the equation `t = t`, where `t` is the type of `u`, which is satisfiable for any type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8137#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8137: Permited mega-polymorphic type ------------------------------------------------+-------------------------- Reporter: wvv | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.6.3 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts invalid program | Unknown/Multiple Test Case: | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: ------------------------------------------------+-------------------------- Comment (by carter): indeed. Wvv, please direct your type system dialogues to #haskell, the haskell- cafe mailing lists, related community fora. You're still learning about type theory, and while the interest is appreciated, ghc trac isn't the appropriate forum for that. thanks -Carter -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8137#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC