#8669 closed bug (invalid)

Closed TypeFamilies regression

Reported by: merijn Owned by:
Priority: high Milestone:
Component: Compiler Version: 7.7
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect result at runtime Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

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).

Change History (2)

comment:1 Changed 18 months ago 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

comment:2 Changed 18 months ago by goldfire

  • Resolution set to invalid
  • Status changed from new to closed

(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 ().

  1. 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!)
  1. 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.

Note: See TracTickets for help on using tickets.