Infinite loop in compiler without undecidableXXX

The following code causes the compiler to loop.

{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}
{-# LANGUAGE KindSignatures, MultiParamTypeClasses, TypeFamilies, TypeOperators #-}

module Arithmetic where

import Data.Monoid ((<>))

data Product :: [*] -> * where
    (:*) :: a -> Product as -> Product (a : as)
    Unit :: Product '[]
infixr 5 :* 

instance Show (Product '[]) where
    show Unit = "Unit"

instance (Show a, Show (Product as)) => Show (Product (a : as)) where
    show (a :* as) = show a <> " :* " <> show as

class Divideable a as where
    type Divide a as :: [*]
    divide :: Product as -> (a, Product (Divide a as))

instance Divideable a (a : as) where
    -- type Divide a (a : as) = as
    -- Conflicting type family instances, seems like OVERLAPS isn't a thing for type families.
    divide (a :* as) = (a, as) 

instance Divideable b as => Divideable b (a : as) where
    type Divide b (a : as) = a : Divide b as
    divide (a :* as) = a :* divide as

Looks like it is because it is erroneously trying to solve as ~ Product (Divide a as) in order to type check divide.

This bug has been fixed in more recent versions of GHC.

Trac metadata

Trac field	Value
Version	8.0.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

changed milestone to %8.2.1

Do we have a test case for this yet?

This was fixed in commit 1eec1f21 (Another major constraint-solver refactoring). In particular, this reminds me a lot of #12538 (closed), wherein overlapping multi-parameter type classes with type families also resulted in an infinite loop at compile-time.

mentioned in commit 6597f084

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added Pnormal label