[GHC] #13295: Failure to resolve type parameter determined by type family
#13295: Failure to resolve type parameter determined by type family -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | 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: -------------------------------------+------------------------------------- {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} import Data.Proxy -- Defined to get the type forall x . 'D x data D where D :: a -> D type family F t :: D -- Will try to create values of this type through the type family -- F, i.e. G (F t) data G (d :: D) where G :: G ('D x) -- This is rejected because the type variable x in 'D x is ambiguous. -- But is it really? If there's an instance of F t then x is determined. introG :: Proxy t -> G (F t) introG _ = G -- introG is well-typed if we add an equality constraint. -- Can GHC not figure this out without our help? introG' :: forall t x . ( F t ~ 'D x ) => Proxy t -> G (F t) introG' _ = G }}} Here's the type error: {{{ • Couldn't match type ‘F t’ with ‘'D x0’ Expected type: G (F t) Actual type: G ('D x0) The type variable ‘x0’ is ambiguous • In the expression: G In an equation for ‘introG’: introG _ = G }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13295 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13295: Failure to resolve type parameter determined by type family -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 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 goldfire): The error is poor (ambiguity isn't really the issue), but I agree that GHC should reject your first function but accept your second. Your first function relies critically on the fact that `D` has but one constructor. Thus, we know that an element of `D` is constructed with `'D`. Without this knowledge, then `introG` really is problematic. Although we believe it's sound to do so, GHC does not currently do this kind of reasoning (i.e., eta-expansion). In `introG'`, the type signature tells us that `F t` evaluates to a use of `'D`, so the missing piece is provided. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13295#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13295: Failure to resolve type parameter determined by type family -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 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 simonpj): It's not just that GHC doesn't do this kind of reasoning; it's also that system FC does not (yet, anyway) have a way to express the evidence. What you want to say is "for any type `t`, `F t` must be equal to `'D s` for some type `s`". But * If `F` has no instances that statement isn't true; `F t` isn't equal to any type other than `F t`. * Even if it does, we'd need an axiom of form {{{ forall t. F t ~ (exists s. 'D s) }}} and we have no such form. So I think this is well out of reach just at the moment. Not wrong; just out of reach. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13295#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13295: Failure to resolve type parameter determined by type family -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 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 alexvieth): I see. So the necessary theoretical work just hasn't been done. I hope that eventually `introG` can be accepted, but in the mean-time, perhaps we could come up with a more helpful error message? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13295#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13295: Failure to resolve type parameter determined by type family -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 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 RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13295#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC