[GHC] #9898: Couldn't match type `(Char, ())' with `()'
#9898: Couldn't match type `(Char, ())' with `()' -------------------------------------+------------------------------------- Reporter: erisco | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Operating System: Windows Keywords: | Type of failure: GHC Architecture: x86_64 (amd64) | rejects valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- 'test3' is expected to type check given that 'test1' and 'test2' type check. 'test4' is not expected to type check. {{{ ghc_bug2.hs:24:9: Couldn't match type `(Char, ())' with `()' Expected type: Filter (Equal Int) (Char, Filter (Equal Int) ()) Actual type: () In the expression: () :: Filter (Equal Int) (Char, Filter (Equal Int) ()) In an equation for `test2': test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ()) ghc_bug2.hs:28:9: Couldn't match type `(Char, ())' with `()' Expected type: Filter (Equal Int) (Char, ()) Actual type: () In the expression: () In an equation for `test3': test3 = () }}} {{{#!hs {-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds #-} module Main where type family Filter f xs where Filter f (x, xs) = ApplyFilter (f x) (x, Filter f xs) Filter f () = () -- type family ApplyFilter p xs where ApplyFilter False (x, xs) = xs ApplyFilter p xs = xs -- type family Equal x y where Equal x x = True Equal x y = False -- -- Type checks test1 :: ApplyFilter ((Equal Int) Char) (Char, Filter (Equal Int) ()) test1 = () -- Couldn't match type `(Char, ())' with `()' test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ()) -- Couldn't match type `(Char, ())' with `()' test3 :: Filter (Equal Int) (Char, ()) test3 = () -- Type checks, should not test4 :: Filter (Equal Int) (Char, ()) test4 = ('x', ()) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: x86_64 (amd64) Resolution: | Difficulty: Unknown Operating System: Windows | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by simonpj): * type: bug => feature request Comment: HEAD correctly says {{{ T9898.hs:20:10: Type family ‘Equal’ should have 2 arguments, but has been given 1 In the type signature for ‘test1’: test1 :: ApplyFilter ((Equal Int) Char) (Char, Filter (Equal Int) ()) T9898.hs:27:10: Type family ‘Equal’ should have 2 arguments, but has been given 1 In the type signature for ‘test3’: test3 :: Filter (Equal Int) (Char, ()) T9898.hs:31:10: Type family ‘Equal’ should have 2 arguments, but has been given 1 In the type signature for ‘test4’: test4 :: Filter (Equal Int) (Char, ()) }}} You can't partially apply a type function, I'm afraid. Yes, that limits higher-order programming. Better solutions (that still support type inference) most welcome. I'll leave this open as a feature request for higher order type level programming. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: x86_64 (amd64) Resolution: | Difficulty: Unknown Operating System: Windows | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by erisco): Thanks Simon. I was mislead by the problem reported in issue #9433. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: x86_64 (amd64) Resolution: | Difficulty: Unknown Operating System: Windows | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Though I'm all for fixing this so that it's possible in GHC, you may also want to check out the `singletons` package, which goes to lengths to emulate this feature. See also the related paper [http://www.cis.upenn.edu/~eir/papers/2014/promotion/promotion.pdf here]. One of these years, I hope to push for adoption of some of the ideas from that paper into GHC proper -- without defunctionalization, for sure. See sections 7.2 and 7.5. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: x86_64 (amd64) Resolution: | Difficulty: Unknown Operating System: Windows | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by erisco): Does applying a type family to no arguments count as being partially applied? i.e. will such usage be banned n 7.8.4? So far 7.8.3 seems to make correct inferences in such cases. If this breaks in 7.8.4 I would like to know so that I do not write a lot of code that depends on it. Compiling GHC does not appear to be a small task otherwise I would test it myself. Here is an example where it is relevant. Maybe there is a better implementation. A usage may be `F EvalEqual :. F (Equal Int) :: Fun * Bool` which can then be used as a predicate for filtering a type list, for example. Of course a possible problem is that `EvalEqual` may be considered partially applied and rejected by 7.8.4 even though this appears to work fine in 7.8.3 (i.e. inference appears to be working fine). {{{ data Equal' where Equal :: x -> y -> Equal' type family EvalEqual (x :: Equal') :: Bool where EvalEqual (Equal x x) = True EvalEqual (Equal x y) = False }}} For completeness here are the other definitions, and I include `:$` as well. Not sure if this is the way to do function composition but this is the best I have after a few failed attempts. {{{ data Fun a b where F :: (a -> b) -> Fun a b (.:) :: Fun b c -> Fun a b -> Fun a c type family (f :: Fun ka kb) :$ (x :: ka) where (f .: g) :$ x = g :$ (f :$ x) (F f) :$ x = f x }}} What is a good place for Q&A on type level programming in Haskell? Obviously the GHC bug tracker is not it. I have tried the #haskell IRC channel but there are only a few people there that understand this area and I can seldom get their attention. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: x86_64 (amd64) Resolution: | Difficulty: Unknown Operating System: Windows | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by jstolarek):
Does applying a type family to no arguments count as being partially applied? Yes. To be more precise: you can't have *unsaturated* type families, where unsaturated means "applied to less arguments than it's arity".
will such usage be banned n 7.8.4? No. But that's still a bug and you shouldn't construct your code around this.
What is a good place for Q&A on type level programming in Haskell? Haskell-cafe.
If you really want partial application at the type level you can try out `singletons`, as suggested by Richard. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
will such usage be banned n 7.8.4? No. But that's still a bug and you shouldn't construct your code around
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: x86_64 (amd64) Resolution: | Difficulty: Unknown Operating System: Windows | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by rwbarton): Replying to [comment:5 jstolarek]: this. Really? #9433 is marked as merged as 7.8.4, or am I misunderstanding something here? Or is there a distinction between the "applied to zero arguments" case and the "applied to at least one, but fewer than its arity" case? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: x86_64 (amd64) Resolution: | Difficulty: Unknown Operating System: Windows | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by jstolarek): Replying to [comment:6 rwbarton]:
Really? #9433 is marked as merged as 7.8.4 You're right. In that case this behaviour will change in GHC 7.8.4. I don't know why, but my impression was that 7.8.4 will only address some critical LLVM bug.
Or is there a distinction between the "applied to zero arguments" case and the "applied to at least one, but fewer than its arity" case? No, that's the same.
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Changes (by thomie): * os: Windows => Unknown/Multiple * architecture: x86_64 (amd64) => Unknown/Multiple -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * cc: kcsongor (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): See also [https://github.com/ghc-proposals/ghc-proposals/pull/52 this GHC proposal] on partially applied type families, which is quite relevant here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9898: Wanted: higher-order type-level programming -------------------------------------+------------------------------------- Reporter: erisco | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => TypeFamilies -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9898#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC