Opened 2 years ago

Closed 2 years ago

#10488 closed bug (fixed)

Inconsistent reduction of type family

Reported by: goldfire Owned by:
Priority: highest Milestone: 7.10.2
Component: Compiler Version: 7.10.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Phab:D955 Differential Rev(s):
Wiki Page:

Description

Consider this module:

{-# LANGUAGE TemplateHaskell, TypeFamilies, GADTs, PolyKinds, DataKinds,
             ScopedTypeVariables, TypeOperators, UndecidableInstances #-}

module SingBug where

import Data.Singletons.TH

$(promote [d|
  data Nat = Zero | Succ Nat
    deriving (Eq, Ord)
  |])

foo :: Proxy (Zero :< Succ Zero)
foo = (Proxy :: Proxy True)

It fails to compile, with this:

SingBug.hs:14:8:
    Couldn't match type ‘'False’ with ‘'True’
    Expected type: Proxy ('Zero :< 'Succ 'Zero)
      Actual type: Proxy 'True
    In the expression: (Proxy :: Proxy True)
    In an equation for ‘foo’: foo = (Proxy :: Proxy True)

However, if I remove the last two lines, it compiles fine. Witness this bizarre interaction:

Prelude> :load "SingBug.hs"
[1 of 1] Compiling SingBug          ( SingBug.hs, interpreted )
Ok, modules loaded: SingBug.
*SingBug> :kind! Zero :< Succ Zero
Zero :< Succ Zero :: Bool
= TrueSym0
*SingBug> :i TrueSym0
type TrueSym0 = 'True
  	-- Defined in ‘singletons-1.2:Data.Singletons.Prelude.Instances’
*SingBug> :kind! (Proxy (Zero :< Succ Zero))
(Proxy (Zero :< Succ Zero)) :: *
= Proxy TrueSym0
*SingBug> :t (Proxy :: Proxy (Zero :< Succ Zero))
(Proxy :: Proxy (Zero :< Succ Zero))
  :: Proxy ('Zero :< 'Succ 'Zero)
*SingBug> :t (Proxy :: Proxy (Zero :< Succ Zero)) :: Proxy True

<interactive>:1:2:
    Couldn't match type ‘'False’ with ‘'True’
    Expected type: Proxy 'True
      Actual type: Proxy ('Zero :< 'Succ 'Zero)
    In the expression:
        (Proxy :: Proxy (Zero :< Succ Zero)) :: Proxy True
*SingBug> :t (Proxy :: Proxy (Zero :< Succ Zero)) :: Proxy False
(Proxy :: Proxy (Zero :< Succ Zero)) :: Proxy False :: Proxy 'False

It seems GHC can't decide if 0 is less than 1! When I ask it to use :kind!, it does the right thing. But if it's reducing a type during type-checking, it does very much the wrong thing.

This is a regression compared to 7.8.

I've been unable to minimize the test case or remove the singletons dependency, sadly. When I try to mimic the behavior of singletons without TH, it all works as expected.

But I've found the problem. The apartness check for closed type families is very subtly broken, and I believe you can break the type system exploiting this bug. I can't quite tickle it directly though. Fix on the way in the next day.

Change History (5)

comment:1 Changed 2 years ago by thoughtpolice

Status: newpatch

comment:2 Changed 2 years ago by Richard Eisenberg <eir@…>

In 761fb7c4869a081da7320e4307dcb947b5ed95d1/ghc:

Fix #10488 by unwrapping type synonyms.

Summary:
Previously, I had forgotten to unwrap vanilla type synonyms in the
"flattener" that is used around the closed-type-family apartness
check.

Test Plan: validate

Reviewers: austin

Subscribers: bgamari, thomie

Differential Revision: https://phabricator.haskell.org/D955

GHC Trac Issues: #10488

comment:3 Changed 2 years ago by goldfire

Status: patchmerge

This is a nasty bug (that is, utterly broken type system) with a very easy fix. Please merge. Thanks!

comment:4 Changed 2 years ago by goldfire

No test case added, as I was unable to tickle the bug without singletons. Besides, the fix is so straightforward, I'm not worried about a regression here.

comment:5 Changed 2 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Merged to ghc-7.10!

Note: See TracTickets for help on using tickets.