Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,322
    • Issues 4,322
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 366
    • Merge Requests 366
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #8669

Closed
Open
Opened Jan 14, 2014 by Merijn Verstraaten@merijnReporter

Closed TypeFamilies regression

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).
Trac metadata
Trac field Value
Version 7.7
Type Bug
TypeOfFailure OtherFailure
Priority high
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#8669