Commit 04613055 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

Fix bug in the short-cut solver

Trac #13943 showed that the relatively-new short-cut solver
for class constraints (aka -fsolve-constant-dicts) was wrong.
In particular, see "Type families" under Note [Shortcut solving]
in TcInteract.

The short-cut solver recursively solves sub-goals, but it doesn't
flatten type-family applications, and as a result it erroneously
thought that C (F a) cannot possibly match (C 0), which is
simply untrue.  That led to an inifinte loop in the short-cut
solver.

The significant change is the one line

+                 , all isTyFamFree preds  -- See "Type families" in
+                                          -- Note [Shortcut solving]

but, as ever, I do some other refactoring.  (E.g. I changed the
name of the function to shortCutSolver rather than the more
generic trySolveFromInstance.)

I also made the short-cut solver respect the solver-depth limit,
so that if this happens again it won't just produce an infinite
loop.

A bit of other refactoring, notably moving isTyFamFree
from TcValidity to TcType

(cherry picked from commit a8fde183)
parent 876fec04
This diff is collapsed.
......@@ -99,7 +99,7 @@ module TcType (
isImprovementPred,
-- * Finding type instances
tcTyFamInsts,
tcTyFamInsts, isTyFamFree,
-- * Finding "exact" (non-dead) type variables
exactTyCoVarsOfType, exactTyCoVarsOfTypes,
......@@ -813,6 +813,10 @@ tcTyFamInsts (CastTy ty _) = tcTyFamInsts ty
tcTyFamInsts (CoercionTy _) = [] -- don't count tyfams in coercions,
-- as they never get normalized, anyway
isTyFamFree :: Type -> Bool
-- ^ Check that a type does not contain any type family applications.
isTyFamFree = null . tcTyFamInsts
{-
************************************************************************
* *
......@@ -1289,7 +1293,7 @@ mkInfSigmaTy tyvars ty = mkSigmaTy (mkTyVarBinders Inferred tyvars) ty
-- | Make a sigma ty where all type variables are "specified". That is,
-- they can be used with visible type application
mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
mkSpecSigmaTy tyvars ty = mkSigmaTy (mkTyVarBinders Specified tyvars) ty
mkSpecSigmaTy tyvars preds ty = mkSigmaTy (mkTyVarBinders Specified tyvars) preds ty
mkPhiTy :: [PredType] -> Type -> Type
mkPhiTy = mkFunTys
......
......@@ -1768,10 +1768,6 @@ checkValidTypePat pat_ty
; checkTc (isTyFamFree pat_ty) $
tyFamInstIllegalErr pat_ty }
isTyFamFree :: Type -> Bool
-- ^ Check that a type does not contain any type family applications.
isTyFamFree = null . tcTyFamInsts
-- Error messages
wrongNumberOfParmsErr :: Arity -> SDoc
......
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE GADTs #-}
module Data.List.Unrolled where
import GHC.TypeLits
-- | Drop @n@ elements from a list
class Drop (n :: Nat) where
drop :: [a] -> [a]
instance {-# OVERLAPPING #-} Drop 0 where
drop xs = xs
{-# INLINE drop #-}
instance {-# OVERLAPPABLE #-} (Drop (n - 1)) => Drop n where
drop [] = []
drop (_ : xs) = drop @(n - 1) xs
{-# INLINE drop #-}
-- | Take @n@ elements from a list
class Take (n :: Nat) where
take :: [a] -> [a]
instance {-# OVERLAPPING #-} Take 0 where
take _ = []
{-# INLINE take #-}
instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where
take [] = []
take (x : xs) = x : take @(n - 1) xs
{-# INLINE take #-}
-- | Split list at @n@-th element.
splitAt :: forall (n :: Nat) a. (Take n, Drop n) => [a] -> ([a], [a])
splitAt xs = (take @n xs, drop @n xs)
-- | Split list into chunks of the given length @c@. @n@ is length of the list.
class ChunksOf (n :: Nat) (c :: Nat) where
chunksOf :: [a] -> [[a]]
instance {-# OVERLAPPING #-} ChunksOf 0 0 where
chunksOf _ = []
{-# INLINE chunksOf #-}
instance {-# OVERLAPPABLE #-} ChunksOf 0 c where
chunksOf _ = []
{-# INLINE chunksOf #-}
instance {-# OVERLAPPABLE #-} ChunksOf n 0 where
chunksOf _ = []
{-# INLINE chunksOf #-}
instance {-# OVERLAPPABLE #-} (Take c, Drop c, ChunksOf (n - 1) c) => ChunksOf n c where
chunksOf xs =
let (l, r) = splitAt @c xs
in l : chunksOf @(n - 1) @c r
{-# INLINE chunksOf #-}
......@@ -564,3 +564,4 @@ test('T13984', normal, compile, [''])
test('T14128', normal, multimod_compile, ['T14128Main', '-v0'])
test('T14154', normal, compile, [''])
test('T14158', normal, compile, [''])
test('T13943', normal, compile, ['-fsolve-constant-dicts'])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment