[GHC] #8669: Closed TypeFamilies regression
#8669: Closed TypeFamilies regression --------------------------+------------------------------------------------ Reporter: merijn | Owner: Type: bug | Status: new Priority: high | Milestone: Component: | Version: 7.7 Compiler | Operating System: Unknown/Multiple Keywords: | Type of failure: Incorrect result at runtime Architecture: | Test Case: Unknown/Multiple | Blocking: Difficulty: | Unknown | Blocked By: | Related Tickets: | --------------------------+------------------------------------------------ I first played around with closed typefamilies early 2013 and wrote up the following simple example {{{ {-# LANGUAGE ConstraintKinds, DataKinds, PolyKinds, TypeFamilies, TypeOperators #-} import GHC.Prim (Constraint) type family Restrict (a :: k) (as :: [k]) :: Constraint type instance where Restrict a (a ': as) = (a ~ "Oops! Tried to apply a restricted type!") Restrict x (a ': as) = Restrict x as Restrict x '[] = () foo :: Restrict a '[(), Int] => a -> a foo = id }}} This worked fine, functioning like `id` for types other than `()` and `Int` and returning a type error for `()` and `Int`. After hearing comments that my example broke when the closed type families syntax changed I decided to update my version of 7.7 and change the code for that. The new code is: {{{ {-# LANGUAGE ConstraintKinds, DataKinds, PolyKinds, TypeFamilies, TypeOperators #-} import GHC.Prim (Constraint) type family Restrict (a :: k) (as :: [k]) :: Constraint where Restrict a (a ': as) = (a ~ "Oops! Tried to apply a restricted type!") Restrict x (a ': as) = Restrict x as Restrict x '[] = () foo :: Restrict a '[(), Int] => a -> a foo = id }}} This code is accepted by the compiler just fine, but the `Constraint` gets thrown out. When querying ghci for the type of `foo` the following is returned: {{{ λ :t foo foo :: a -> a λ :i foo foo :: (Restrict a '[(), Int]) => a -> a }}} Additionally, in the recent 7.7 `foo ()` returns `()` rather than a type error. After some playing around this seems to be caused by the "(a ~ "Oops! Tried to apply a restricted type!")" equality constraint. It seems GHC decides that it doesn't like the fact that types with a polymorphic kind and `Symbol` kind are compared. Leading it to silently discard the `Constraint`. This raises two issues: 1) This should probably produce an error, rather than silently discarding the `Constraint` 2) A better way to produce errors in type families is needed, personally I would love an "error" `Constraint` that takes a `String`/`Symbol` and never holds, producing it's argument `String` as type error (This would remove the need for the hacky unification with `Symbol` to get a somewhat relevant type error). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8669 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8669: Closed TypeFamilies regression ------------------------------------------------+-------------------------- Reporter: merijn | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result at runtime | Unknown/Multiple Test Case: | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: ------------------------------------------------+-------------------------- Comment (by simonpj): I know why this happens. If I add the kinds to the definition, I get this: {{{ type family Restrict k (a :: k) (as :: [k]) :: Constraint where Restrict Symbol (a::Symbol) (a ': as) = (a ~ "Oops! Tried to apply a restricted type!") Restrict k (x::k) (a ': as) = Restrict x as Restrict k (x::k) '[] = () }}} The first equation only applies to types of kind `Symbol` because the RHS has an equality that forces `a :: Symbol` since `"Oops" :: Symbol`. The constraint `(Restricted (a:*) [(),Int])` can't match the first equation (because the first equation matches only things of kind `Symbol`, so it correctly chooses the second. What to do? For your (2) how about this: {{{ class Error (s::Symbol) -- No instances }}} Now `Error :: Symbol -> Constraint`, as you wanted, and you can write {{{ type instance where Restrict a (a ': as) = Error "Oops! Tried to apply a restricted type!" Restrict x (a ': as) = Restrict x as Restrict x '[] = () }}} And away you go. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8669#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8669: Closed TypeFamilies regression ------------------------------------------------+-------------------------- Reporter: merijn | Owner: Type: bug | Status: closed Priority: high | Milestone: Component: Compiler | Version: 7.7 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result at runtime | Unknown/Multiple Test Case: | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: ------------------------------------------------+-------------------------- Changes (by goldfire): * status: new => closed * resolution: => invalid Comment: (Written before Simon's post -- I guess we think alike!) I would say that GHC's behavior in this case is correct, for the following reasons: 1. The equality operator `~` is ''homogeneous''. This means that the kinds of the types on both sides must be the same. With this in mind, here is `Restrict`, with all kind variables/arguments made explicit: {{{ type family Restrict (k :: BOX) (a :: k) (as :: [k]) :: Constraint where forall (a :: Symbol) (as :: [Symbol]). Restrict Symbol a (a ': as) = (a ~ "...") forall (k :: BOX) (x :: k) (a :: k) (as :: [k]). Restrict k x (a ': as) = Restrict k x as forall (k :: BOX) (x :: k). Restrict k x ('[] k) = () }}} In your `foo`, the variable `a` surely has kind `*`, not `Symbol`. So, the first equation of `Restrict` does not apply, and GHC correctly reduces the type family away when reporting the type of `foo`, as the constraint always reduces to `()`. 2. You suggest that GHC should produce an error here. But, there's no real way for GHC to know that you're not trying to write a ''kind-indexed'' type family, where matching on the kind really is intentional. Some possible ways forward: 1. Closed type families do full kind inference (unlike open ones), but with a twist: a kind variable used in matching must be declared in a kind annotation. Thus, if you use kind inference only, then you indeed would get an error with a definition like `Restrict`. So, unless you want a kind-indexed type family, you might be best off omitting the kind annotations. (I realize there's a good deal of value in having a kind annotation even if you don't want a kind-indexed type family, but putting in the kind variable opens you up to the possibility of silent unintended behavior in this way. I'm open to suggestions of other ways of distinguishing kind-indexed from non-kind-indexed type families!) 2. With or without kind annotations, you can do something like this: {{{ class False ~ True => Error (x :: Symbol) }}} and then use that in your first equation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8669#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC