#12918: Make DefaultSignatures more particular about their types on the RHS of a context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.2-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12784 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by kosmikus): * cc: kosmikus (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12918#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#12918: Make DefaultSignatures more particular about their types on the RHS of a context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.2-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12784 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:2 simonpj]:

Thanks for making this a new ticket, Ryan. Do you think you might execute on it? I can advise.

Certainly! And since you extended the offer for advice... I could certainly use it :) Some questions that pop into my head: 1. Where is the best place to add this check? [https://git.haskell.org/ghc.git/blob/f5f6d4237b87f5d0e3e0a05e4cfc52bb3c0e4ad... tc_default] in `TcInstDecls`? 2. How stringent should this check be? For instance, should this be accepted? {{{#!hs class Eq1 f where (==#) :: forall a. Eq a => f a -> f a -> Bool default (==#) :: forall b. Eq (f b) => f b -> f b -> Bool (==#) = (==) }}} These have the same tau types module `forall`'d type variable names. Should we require that the type variables be //exactly// the same, even down to the `forall`'d ones? Even in this cleaned up version: {{{#!hs class Eq1 f where (==#) :: forall a. Eq a => f a -> f a -> Bool default (==#) :: forall a. Eq (f a) => f a -> f a -> Bool (==#) = (==) }}} The `a`s get renamed behind the scenes, so it's actually closer to: {{{#!hs class Eq1 f where (==#) :: forall a1. Eq a1 => f a1 -> f a1 -> Bool default (==#) :: forall a2. Eq (f a2) => f a2 -> f a2 -> Bool (==#) = (==) }}} After renaming. 3. How do type families affect this? Currently, there's an accepted GHC testsuite test ([https://git.haskell.org/ghc.git/blob/f5f6d4237b87f5d0e3e0a05e4cfc52bb3c0e4ad... T10361b]) with this default type signature: {{{#!hs class Convert a where type Result a type instance Result a = GResult (Rep a) convert :: a -> Result a default convert :: (Generic a, GConvert (Rep a)) => a -> GResult (Rep a) convert x = gconvert (from x) }}} Should this be rejected now? That is, must you write the above like this? {{{#!hs convert :: a -> Result a default convert :: (Generic a, GConvert (Rep a), Result a ~ GResult (Rep a)) => a -> Result a }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12918#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#12918: Make DefaultSignatures more particular about their types on the RHS of a context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.2-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12784 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): OK, I've made some progress on this, but I'm once again stuck. I'm using `tcUnifyTy` once again to check if two type signatures coincide according to the criteria listed above. But there's a case it doesn't catch: {{{#!hs class Foo a where bar :: forall b. a -> b default bar :: a -> Int bar = ... }}} Here, `tcUnifyTy` happily unifies `b` with `Int`, yielding a false positive. So I need to find some way to prevent `b` from unifying with concrete types like `Int`. (Does skolemizing it accomplish this?) But we'd also want this to be accepted: {{{#!hs class Foo a where bar :: forall b. a -> b default bar :: forall c. a -> c bar = ... }}} Since `a -> c` is just a simple alpha-renaming of `a -> b`. So how can we tell `b` to unify with `c` but not with `Int`? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12918#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#12918: Make DefaultSignatures more particular about their types on the RHS of a context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: simonpj Type: bug | Status: patch Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.2-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12784 | Differential Rev(s): Phab:D2983 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Consider {{{ class C a b where op :: forall p q. (Ord a, D p q) => a -> b -> (a,b) default op :: forall r. (E r) => a -> b -> (a,b) }}} We are expecting the part after the `=>` to be identical. In `check_dm` in `checkValidClass` we have in hand: * `sel_id :: forall aa bb. C aa bb => forall p q. (Ord p, D p q) => aa -> bb -> p -> (aa,bb)`. Note that `sel_id` always has this form: see `sel_ty` in `MkId.mkDictSelId` * Inside class `C a b` we have a `GemericDM (forall r s. (E r) => a -> b -> s -> (a,b)`. This is passed to `check_dm`. Notice that, as commented with `Class.DefMethInfo`, the `ty` in `(GenericDM ty)` is ''not'' quantified over the class variables `a` and `b`. But `sel_id` ''is'' so quantified, and in principle its foralls, here `aa` and `bb`, might be different to the class tyvars `a` and `b`. (This will never happen in practice, but still.) What we want is to match up these two types {{{ From sel_id: C aa bb => aa -> bb -> p -> (aa,bb) From GenericDM: C a b => a -> b -> s -> (a, b) }}} This is a '''one-way match''': use `tcMatchTy`. Not unification! We need the `C a b` part to match up `a` with `aa` and `b` with `bb`. If successful we'll emerge with a mapping `[a -> aa, b -> bb, s -> p]`. Is that enough? No: we need to ensure that each variable in the domain of the substitution maps to a distinct type variable in the range. For example `[s -> Int]` would not be OK. I think `TcValidity.allDistinctTyVars` is what you want. Does that help? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12918#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#12918: Make DefaultSignatures more particular about their types on the RHS of a context -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: simonpj Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.2-rc1 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12784 | Differential Rev(s): Phab:D2983 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: patch => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12918#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler